isIso_iff_of_epi — Mathlib

English

For f: n ⟶ m with Epi f, IsIso f iff n.len = m.len.

Русский

Для f: n ⟶ m с Epi f, IsIso f тогда и только тогда, когда n.len = m.len.

LaTeX

$$$\\\\forall {n,m} (f: n \\\\to m) \\\\[Epi f] \\\Longrightarrow IsIso(f) \\\\Longleftrightarrow n.len = m.len$$$

Lean4

theorem isIso_iff_of_epi {n m : SimplexCategory} (f : n ⟶ m) [hf : Epi f] : IsIso f ↔ n.len = m.len :=
  by
  refine ⟨fun _ ↦ len_eq_of_isIso f, fun h ↦ ?_⟩
  obtain rfl : n = m := by aesop
  rw [epi_iff_surjective] at hf
  exact isIso_of_bijective ⟨by rwa [Finite.injective_iff_surjective], hf⟩

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