toLocallyFiniteOrderTop — Mathlib

English

In a locally finite order with top, the set of elements ≥ a equals the closed interval [a, ⊤].

Русский

В локально конечно упорядоченном множестве с верхней границей множество элементов ≥ a равно замкнутому интервалу [a, ⊤].

LaTeX

$$Ici a = Icc a ⊤$$

Lean4

instance (priority := 100) _root_.LocallyFiniteOrder.toLocallyFiniteOrderTop : LocallyFiniteOrderTop α
    where
  finsetIci b := Icc b ⊤
  finsetIoi b := Ioc b ⊤
  finset_mem_Ici a x := by rw [mem_Icc, and_iff_left le_top]
  finset_mem_Ioi a x := by rw [mem_Ioc, and_iff_left le_top]

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