eq_of_isIso — Mathlib

English

For n,m: natural numbers, if f: ⟦n⟧ ⟶ ⟦m⟧ is an isomorphism, then n = m.

Русский

Для натуральных n,m, если f: ⟦n⟧ ⟶ ⟦m⟧ является изоморфизмом, то n = m.

LaTeX

$$$\\\\forall n,m \\\\in \\\\mathbb{N}, \\\\forall f: \\\\langle n \\\\rangle \\\\to \\\\langle m \\\\rangle,[\\\\text{IsIso } f] \\\Rightarrow n = m$$$

Lean4

theorem eq_of_isIso {n m : ℕ} (f : ⦋n⦌ ⟶ ⦋m⦌) [IsIso f] : n = m :=
  len_eq_of_isIso f

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