instFintypeIoc

Mathlib.Order.Interval.Finset.Defs

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

English

The half-open interval Ico a b is finite.

Русский

Полуоткрытый интервал Ico a b конечно.

LaTeX

$$(Ico a b).Finite$$

Lean4

instance instFintypeIoc : Fintype (Ioc a b) :=
  .ofFinset (Finset.Ioc a b) fun _ => Finset.mem_Ioc

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

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

Разделы

Аффилиация

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