instFintypeIcc

Mathlib.Order.Interval.Finset.Defs

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

English

There is a finite-type instance for Set.Ioo a b, realized by Finset.Ioo a b.

Русский

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

LaTeX

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

Lean4

instance instFintypeIcc : Fintype (Icc a b) :=
  .ofFinset (Finset.Icc a b) fun _ => Finset.mem_Icc

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

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

Разделы

Аффилиация

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