attachFin_Iio

Mathlib.Order.Interval.Finset.Fin

URI: https://scilib.ai/kg/mathlib#Fin.attachFin_Iio

English

In Fin(n), the Iio interval equals the preimage of Iio under the natural projection, i.e., elements less than a.

Русский

В Fin(n) интервал Iio равен подмножеству меньших чем a через естественную проекцию.

LaTeX

$$$\mathrm{Iio}(a) = \{x \in \mathrm{Fin}(n) : x < a\}.$$$

Lean4

@[simp]
theorem attachFin_Iio : attachFin (Iio a) (fun _x hx ↦ (mem_Iio.mp hx).trans a.2) = Iio a := by ext; simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru