Ioi_zero_eq_map — Mathlib

English

In Fin n, the elements greater than 0 correspond exactly to the image of univ under the successor embedding.

Русский

В Fin n элементы, больших 0, соответствуют изображениям единичного элемента под вложением successor.

LaTeX

$$$ \\mathrm{Ioi}(0) = \\mathrm{univ}.\\mathrm{map}(\\mathrm{Fin.succEmb}(n)) $$$

Lean4

@[simp]
theorem Ioi_zero_eq_map : Ioi (0 : Fin n.succ) = univ.map (Fin.succEmb _) :=
  coe_injective <| by ext; simp [pos_iff_ne_zero]

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