instFiniteSubtypeLeOfLocallyFiniteOrderBot

English

If α has Preorder and LocallyFiniteOrderBot, then the set of elements below y, viewed as a subtype, is finite.

Русский

Если у α есть предикаты preorder и LocallyFiniteOrderBot, тогда множество элементов не превышающих y в виде подтипа является конечным.

LaTeX

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

Lean4

instance [Preorder α] [LocallyFiniteOrderBot α] : Finite { x : α // x ≤ y } := by
  simpa only [coe_Iic] using (Finset.Iic y).finite_toSet

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