instFintypeIoo

Mathlib.Order.Interval.Finset.Defs

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

English

The open interval Ioo a b is finite.

Русский

Открытый интервал Ioo a b конечно.

LaTeX

$$(Ioo a b).Finite$$

Lean4

instance instFintypeIoo : Fintype (Ioo a b) :=
  .ofFinset (Finset.Ioo a b) fun _ => Finset.mem_Ioo

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

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

Разделы

Аффилиация

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