coe_Icc

Mathlib.Order.Interval.Finset.Defs

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

English

The Finset Icc(a,b) considered as a set equals the interval Set.Icc(a,b).

Русский

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

LaTeX

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

Lean4

@[simp, norm_cast]
theorem coe_Icc (a b : α) : (Icc a b : Set α) = Set.Icc a b :=
  Set.ext fun _ => mem_Icc

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

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

Разделы

Аффилиация

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