coe_Ico

Mathlib.Order.Interval.Finset.Defs

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

English

The Finset Ico(a,b) coincides with Set.Ico(a,b) when regarded as sets.

Русский

Финсет Ico(a,b), рассматриваемый как множество, совпадает с Set.Ico(a,b).

LaTeX

$$$(Ico(a,b) : Set \alpha) = Set.Ico(a,b)$$

Lean4

@[simp, norm_cast]
theorem coe_Ico (a b : α) : (Ico a b : Set α) = Set.Ico a b :=
  Set.ext fun _ => mem_Ico

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

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

Разделы

Аффилиация

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