eq_id_of_mono — Mathlib

English

If i: x ⟶ x is mono, then i equals the identity on x.

Русский

Если i: x ⟶ x моно, то i равен тождественному на x.

LaTeX

$$$\\\\forall x \\\\in \\\\text{SimplexCategory},\\\\forall i: x \\\\to x,[\\\\text{Mono } i] \\\Rightarrow i = \\mathsf{Id}_x$$$

Lean4

theorem eq_id_of_mono {x : SimplexCategory} (i : x ⟶ x) [Mono i] : i = 𝟙 _ :=
  by
  suffices IsIso i by apply eq_id_of_isIso
  apply isIso_of_bijective
  dsimp
  rw [Fintype.bijective_iff_injective_and_card i.toOrderHom, ← mono_iff_injective, eq_self_iff_true, and_true]
  infer_instance

Похожие утверждения