English
A construction from a definition of Finset.Icc alone, together with a predicate for membership, yields a LocallyFiniteOrder where finsetIco, finsetIoc, finsetIoo are given by removing endpoints as appropriate.
Русский
Конструкция из определения Finset.Icc с помощью предиката принадлежности порождает LocallyFiniteOrder, где уменьшение интервалов осуществляется удалением концов.
LaTeX
$$$\mathrm{LocallyFiniteOrder}(\alpha) := \text{построение из финсет_Icc} (finsetIcc) \text{ и } (\forall a,b,x, x\in 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 `PartialOrder` but only
`DecidableEq`. -/
def ofIcc (α : Type*) [PartialOrder α] [DecidableEq α] (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 | x ≠ b}
finsetIoc a b := {x ∈ finsetIcc a b | a ≠ x}
finsetIoo a b := {x ∈ finsetIcc a b | a ≠ x ∧ x ≠ b}
finset_mem_Icc := mem_Icc
finset_mem_Ico a b x := by rw [Finset.mem_filter, mem_Icc, and_assoc, lt_iff_le_and_ne]
finset_mem_Ioc a b x := by rw [Finset.mem_filter, mem_Icc, and_right_comm, lt_iff_le_and_ne]
finset_mem_Ioo a b x := by rw [Finset.mem_filter, mem_Icc, and_and_and_comm, lt_iff_le_and_ne, lt_iff_le_and_ne]
