equiv_iff_eq — Mathlib

English

There exists an equivalence Fin m ≃ Fin n if and only if m = n.

Русский

Существует эквивалентность Fin m ≃ Fin n тогда и только тогда, когда m = n.

LaTeX

$$$ \exists e: \mathrm{Fin}(m) \cong \mathrm{Fin}(n) \iff m = n $$$

Lean4

theorem equiv_iff_eq : Nonempty (Fin m ≃ Fin n) ↔ m = n :=
  ⟨fun ⟨e⟩ ↦ le_antisymm (nonempty_embedding_iff.1 ⟨e⟩) (nonempty_embedding_iff.1 ⟨e.symm⟩), fun h ↦ h ▸ ⟨.refl _⟩⟩

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