x y : SimplexCategory
f : x ⟶ y
hyp_f_mono : Mono f
⊢ len x ≤ len y
x y : SimplexCategory
f : x ⟶ y
⊢ Mono f → len x ≤ len y
intro hyp_f_mono
x y : SimplexCategory
f : x ⟶ y
hyp_f_mono : Mono f
f_inj : Function.Injective ↑(Hom.toOrderHom f)
⊢ len x ≤ len y
x y : SimplexCategory
f : x ⟶ y
hyp_f_mono : Mono f
⊢ len x ≤ len y
have f_inj : Function.Injective f.toOrderHom.toFun := mono_iff_injective.1 hyp_f_mono
no goals
x y : SimplexCategory
f : x ⟶ y
hyp_f_mono : Mono f
f_inj : Function.Injective ↑(Hom.toOrderHom f)
⊢ len x ≤ len y
simpa using Fintype.card_le_of_injective f.toOrderHom.toFun f_inj