English
A construction from Finset.Ici alone yields a LocallyFiniteOrderTop on α, provided DecidableLE and Preorder are available, with finsetIci governing the upper sets.
Русский
Конструкция LocallyFiniteOrderTop из Finset.Ici и предиката принадлежности, обеспечивающая верхние множества.
LaTeX
$$$\mathrm{LocallyFiniteOrderTop}(\alpha) = \text{конструкция из }finsetIci\text{ с pred: } x\in finsetIci(a) \Leftrightarrow a\le x$$$
Lean4
/-- A constructor from a definition of `Finset.Ici` alone, the other ones being derived by removing
the ends. As opposed to `LocallyFiniteOrderTop.ofIci'`, this one requires `PartialOrder` but
only `DecidableEq`. -/
def ofIci (α : Type*) [PartialOrder α] [DecidableEq α] (finsetIci : α → Finset α)
(mem_Ici : ∀ a x, x ∈ finsetIci a ↔ a ≤ x) : LocallyFiniteOrderTop α
where
finsetIci := finsetIci
finsetIoi a := {x ∈ finsetIci a | a ≠ x}
finset_mem_Ici := mem_Ici
finset_mem_Ioi a x := by rw [mem_filter, mem_Ici, lt_iff_le_and_ne]
