preimage_natAdd_Ici_natAdd

Mathlib.Order.Interval.Set.Fin

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

English

For all m and i in Fin n, the preimage of Ici (natAdd m i) under natAdd m is Ici i.

Русский

Для всех m и i ∈ Fin n, прообраз Ici (natAdd m i) под natAdd m равен Ici i.

LaTeX

$$$\operatorname{natAdd}(m)^{-1}(\mathrm{Ici}(\mathrm{natAdd}(m,i))) = \mathrm{Ici}(i)$$$

Lean4

@[simp]
theorem preimage_natAdd_Ici_natAdd (m) (i : Fin n) : natAdd m ⁻¹' Ici (natAdd m i) = Ici i := by ext; simp

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

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

Разделы

Аффилиация

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