English
A variant of the construction of LocallyFiniteOrder from Icc, using a richer description of membership and intervals; equivalence of certain Iff statements follows.
Русский
Вариант конструкции LocallyFiniteOrder из Icc с более полной характеристикой принадлежности и интервалов; следует эквивалентность определённых утверждений Iff.
LaTeX
$$$\text{…}$$$
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 `DecidableLE` but
only `Preorder`. -/
def ofIci' (α : Type*) [Preorder α] [DecidableLE α] (finsetIci : α → Finset α)
(mem_Ici : ∀ a x, x ∈ finsetIci a ↔ a ≤ x) : LocallyFiniteOrderTop α
where
finsetIci := finsetIci
finsetIoi a := {x ∈ finsetIci a | ¬x ≤ a}
finset_mem_Ici := mem_Ici
finset_mem_Ioi a x := by rw [mem_filter, mem_Ici, lt_iff_le_not_ge]
