orderEmbOfFin_singleton — Mathlib

English

For a singleton {a}, any i ∈ Fin 1 maps to a under orderEmbOfFin.

Русский

Для множества {a} любая позиция i в Fin 1 отображается в a.

LaTeX

$$orderEmbOfFin {a} (card_singleton a) i = a$$

Lean4

/-- `orderEmbOfFin {a} h` sends any argument to `a`. -/
@[simp]
theorem orderEmbOfFin_singleton (a : α) (i : Fin 1) : orderEmbOfFin { a } (card_singleton a) i = a := by
  rw [Subsingleton.elim i ⟨0, Nat.zero_lt_one⟩, orderEmbOfFin_zero _ Nat.zero_lt_one, min'_singleton]

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