preimage_val_Ici_val

Mathlib.Order.Interval.Set.Fin

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

English

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

Русский

Для i ∈ Fin(n) переход через Fin.val от Ici(i) даёт точно Ici(i).

LaTeX

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

Lean4

@[simp]
theorem preimage_val_Ici_val (i : Fin n) : (↑) ⁻¹' Ici (i : ℕ) = Ici i :=
  rfl

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

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

Разделы

Аффилиация

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