iso_eq_iso_refl — Mathlib

English

If e: x ≅ x is an isomorphism, then e = Iso.refl x.

Русский

Если e: x ≅ x является изоморфизмом, то e = Iso.refl x.

LaTeX

$$$\\\\forall x \\\\in \\\\text{SimplexCategory},\\\\forall e: x \\\\cong x, e = \\\\text{Iso.refl } x$$$

Lean4

theorem iso_eq_iso_refl {x : SimplexCategory} (e : x ≅ x) : e = Iso.refl x :=
  by
  have h : (Finset.univ : Finset (Fin (x.len + 1))).card = x.len + 1 := Finset.card_fin (x.len + 1)
  have eq₁ := Finset.orderEmbOfFin_unique' h fun i => Finset.mem_univ ((orderIsoOfIso e) i)
  have eq₂ := Finset.orderEmbOfFin_unique' h fun i => Finset.mem_univ ((orderIsoOfIso (Iso.refl x)) i)
  ext : 2
  convert congr_arg (fun φ => (OrderEmbedding.toOrderHom φ)) (eq₁.trans eq₂.symm)
  ext i : 2
  rfl

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