preimage_castSucc_Iic_castSucc

Mathlib.Order.Interval.Set.Fin

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

English

For any i ∈ Fin n, the preimage of Iic i.castSucc under castSucc equals Iic i.

Русский

Для любого i ∈ Fin n, прообраз Iic i.castSucc под castSucc равен Iic i.

LaTeX

$$$ \operatorname{Set.preimage}(\operatorname{Fin.castSucc})\, (\operatorname{Set.Iic} i.castSucc) = \operatorname{Iic} i $$$

Lean4

@[simp]
theorem preimage_castSucc_Iic_castSucc (i : Fin n) : castSucc ⁻¹' Iic i.castSucc = Iic i :=
  rfl

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

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

Разделы

Аффилиация

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