x y : SimplexCategory
f : x ⟶ y
hyp_f_epi : Epi f
⊢ len y ≤ len x
x y : SimplexCategory
f : x ⟶ y
⊢ Epi f → len y ≤ len x
intro hyp_f_epi
x y : SimplexCategory
f : x ⟶ y
hyp_f_epi : Epi f
f_surj : Function.Surjective ↑(Hom.toOrderHom f)
⊢ len y ≤ len x
x y : SimplexCategory
f : x ⟶ y
hyp_f_epi : Epi f
⊢ len y ≤ len x
have f_surj : Function.Surjective f.toOrderHom.toFun := epi_iff_surjective.1 hyp_f_epi
no goals
x y : SimplexCategory
f : x ⟶ y
hyp_f_epi : Epi f
f_surj : Function.Surjective ↑(Hom.toOrderHom f)
⊢ len y ≤ len x
simpa using Fintype.card_le_of_surjective f.toOrderHom.toFun f_surj