preimage_val_Ioo_val

Mathlib.Order.Interval.Set.Fin

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

English

For i, j ∈ Fin n, the preimage of Ioo(i, j) under Fin.val is Ioo(i, j).

Русский

Для i, j ∈ Fin(n) предобразование Ioo(i, j) по Fin.val совпадает с Ioo(i, j).

LaTeX

$$$$ \operatorname{Set.preimage}(\operatorname{Fin.val}, \operatorname{Set.Ioo}(i, j)) = \operatorname{Ioo}(i, j). $$$$

Lean4

@[simp]
theorem preimage_val_Ioo_val (i j : Fin n) : (↑) ⁻¹' Ioo (i : ℕ) j = Ioo i j :=
  rfl

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

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

Разделы

Аффилиация

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