English
From a definition of Finset.Icc and a decidable LE, together with a predicate that Finset.Icc(a,b) contains exactly the elements between a and b, one constructs a LocallyFiniteOrder with Icc governing its finite intervals.
Русский
Из определения Finset.Icc и decidable LE, вместе с предикатом, что Finset.Icc(a,b) содержит все элементы между a и b, строится LocallyFiniteOrder, где Icc описывает конечные интервалы.
LaTeX
$$$\text{LocallyFiniteOrder}(\alpha)$ построено из финсета $\mathrm{finsetIcc}$ с условием $x\in\mathrm{finsetIcc}(a,b) \iff a\le x \le b$$$
Lean4
/-- A constructor from a definition of `Finset.Icc` alone, the other ones being derived by removing
the ends. As opposed to `LocallyFiniteOrder.ofIcc`, this one requires `DecidableLE` but
only `Preorder`. -/
def ofIcc' (α : Type*) [Preorder α] [DecidableLE α] (finsetIcc : α → α → Finset α)
(mem_Icc : ∀ a b x, x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b) : LocallyFiniteOrder α
where
finsetIcc := finsetIcc
finsetIco a b := {x ∈ finsetIcc a b | ¬b ≤ x}
finsetIoc a b := {x ∈ finsetIcc a b | ¬x ≤ a}
finsetIoo a b := {x ∈ finsetIcc a b | ¬x ≤ a ∧ ¬b ≤ x}
finset_mem_Icc := mem_Icc
finset_mem_Ico a b x := by rw [Finset.mem_filter, mem_Icc, and_assoc, lt_iff_le_not_ge]
finset_mem_Ioc a b x := by rw [Finset.mem_filter, mem_Icc, and_right_comm, lt_iff_le_not_ge]
finset_mem_Ioo a b x := by rw [Finset.mem_filter, mem_Icc, and_and_and_comm, lt_iff_le_not_ge, lt_iff_le_not_ge]
