coe_Ioi

Mathlib.Order.Interval.Finset.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp, norm_cast]
theorem coe_Ioi (a : α) : (Ioi a : Set α) = Set.Ioi a :=
  Set.ext fun _ => mem_Ioi

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

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

Разделы

Аффилиация

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