fin_injective — Mathlib

English

The mapping Fin: ℕ → Type is injective; i.e., Fin m = Fin n implies m = n.

Русский

Отображение Fin: ℕ → Type инъективно; то есть Fin m = Fin n означает m = n.

LaTeX

$$$\text{Injective}(\mathrm{Fin})$$$

Lean4

/-- `Fin` as a map from `ℕ` to `Type` is injective. Note that since this is a statement about
equality of types, using it should be avoided if possible. -/
theorem fin_injective : Function.Injective Fin := fun m n h =>
  (Fintype.card_fin m).symm.trans <| (Fintype.card_congr <| Equiv.cast h).trans (Fintype.card_fin n)

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