n m : SimplexCategory
f : n ⟶ m
⊢ Mono (skeletalEquivalence.functor.map f) ↔ Function.Injective ↑(Hom.toOrderHom f)
n m : SimplexCategory
f : n ⟶ m
⊢ Mono f ↔ Function.Injective ↑(Hom.toOrderHom f)
rw [← Functor.mono_map_iff_mono skeletalEquivalence.functor.{0}]
n m : SimplexCategory
f : n ⟶ m
⊢ Mono (skeletalFunctor.map f) ↔ Function.Injective ↑(Hom.toOrderHom f)
n m : SimplexCategory
f : n ⟶ m
⊢ Mono (skeletalEquivalence.functor.map f) ↔ Function.Injective ↑(Hom.toOrderHom f)
dsimp only [skeletalEquivalence, Functor.asEquivalence_functor]
no goals
n m : SimplexCategory
f : n ⟶ m
⊢ Mono (skeletalFunctor.map f) ↔ Function.Injective ↑(Hom.toOrderHom f)
rw [NonemptyFinLinOrdCat.mono_iff_injective, skeletalFunctor.coe_map,
  Function.Injective.of_comp_iff ULift.up_injective,
  Function.Injective.of_comp_iff' _ ULift.down_bijective]