instFintypeIco

Mathlib.Order.Interval.Finset.Defs

URI: https://scilib.ai/kg/mathlib#Set.instFintypeIco

English

The closed interval Icc a b is finite.

Русский

Замкнутый интервал Icc a b конечно.

LaTeX

$$(Icc a b).Finite$$

Lean4

instance instFintypeIco : Fintype (Ico a b) :=
  .ofFinset (Finset.Ico a b) fun _ => Finset.mem_Ico

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

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

Разделы

Аффилиация

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