coe_uIcc

Mathlib.Order.Interval.Finset.Defs

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

English

There is a finite-type instance for Set.Ico a b, given by Finset.Ico a b.

Русский

Для Set.Ico a b существует инстанс конечного типа, заданный Finset.Ico a b.

LaTeX

$$Fintype (Set.Ico a b)$$

Lean4

@[simp, norm_cast]
theorem coe_uIcc (a b : α) : (Finset.uIcc a b : Set α) = Set.uIcc a b :=
  coe_Icc _ _

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

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

Разделы

Аффилиация

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