instFiniteSubtypeLtOfLocallyFiniteOrderTop

English

The finite-interval top subtype yields a finite set of elements strictly between two bounds in a LocallyFiniteOrderTop.

Русский

По локально конечному порядку над верхом получаем конечное множество элементов строго между двумя границами.

LaTeX

$$$\\text{Finite}\\{ x \\in \\alpha \\mid a < x < b\\}$ under LocallyFiniteOrderTop$$

Lean4

instance [Preorder α] [LocallyFiniteOrderTop α] : Finite { x : α // y < x } := by
  simpa only [coe_Ioi] using (Finset.Ioi y).finite_toSet

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