instFiniteSubtypeLtOfLocallyFiniteOrderBot

Mathlib.Order.Interval.Finset.Defs

URI: https://scilib.ai/kg/mathlib#instFiniteSubtypeLtOfLocallyFiniteOrderBot

English

For any fixed y, the subtype { x | x ≤ y } is finite under LocallyFiniteOrderBot, etc.

Русский

Для фиксированного y подтип { x | x ≤ y } конечен в условиях LocallyFiniteOrderBot и аналогично.

LaTeX

$$$\\text{Finite}\\{ x \\in \\alpha \\mid x \\le y\\}$$$

Lean4

instance [Preorder α] [LocallyFiniteOrderBot α] : Finite { x : α // x < y } := by
  simpa only [coe_Iio] using (Finset.Iio y).finite_toSet

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

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

Разделы

Аффилиация

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