Iio_last_eq_map — Mathlib

English

The set of elements less than the last element of Fin n corresponds to the image of univ under castSuccEmb.

Русский

Множество элементов меньше последнего элемента Fin n соответствует изображению univ под castSuccEmb.

LaTeX

$$$ \\mathrm{Iio}(\\mathrm{Fin}.\\mathrm{last}(n)) = \\mathrm{univ}.\\mathrm{map}(\\mathrm{Fin.castSuccEmb}) $$$

Lean4

@[simp]
theorem Iio_last_eq_map : Iio (Fin.last n) = Finset.univ.map Fin.castSuccEmb :=
  coe_injective <| by ext; simp [lt_def]

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