Iic_eq_finset_subtype

Mathlib.Order.Interval.Finset.Fin

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

English

Iic(b) in Fin(n) equals fin(n) of Iic(b.val).

Русский

Iic(b) в Fin(n) равен fin(n) от Iic(b.val).

LaTeX

$$$\mathrm{Iic}(b) = \mathrm{fin}(n)(\mathrm{Iic}(b.val)).$$$

Lean4

@[deprecated attachFin_Iic (since := "2025-04-06")]
theorem Iic_eq_finset_subtype : Iic b = (Iic (b : ℕ)).fin n := by ext; simp

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

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

Разделы

Аффилиация

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