coe_Ici

Mathlib.Order.Interval.Finset.Defs

URI: https://scilib.ai/kg/mathlib#Finset.coe_Ici

English

Ici(a) as a set equals Set.Ici(a).

Русский

Ici(a), рассматриваемое как множество, равно Set.Ici(a).

LaTeX

$$$(Ici(a) : Set \alpha) = Set.Ici(a)$$

Lean4

@[simp, norm_cast]
theorem coe_Ici (a : α) : (Ici a : Set α) = Set.Ici a :=
  Set.ext fun _ => mem_Ici

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

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

Разделы

Аффилиация

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