English
A construction from Finset.Iic alone yields a LocallyFiniteOrderBot on α, given DecidableLE and Preorder, with finsetIic describing the lower bounds.
Русский
Конструкция LocallyFiniteOrderBot из Finset.Iic с предикатом принадлежности, задающим нижние границы.
LaTeX
$$$\mathrm{LocallyFiniteOrderBot}(\alpha) = \text{конструкция из }finsetIic\text{ с pred: } x\in finsetIic(a) \Leftrightarrow x\le a$$$
Lean4
/-- A constructor from a definition of `Finset.Iic` alone, the other ones being derived by removing
the ends. As opposed to `LocallyFiniteOrderBot.ofIic`, this one requires `DecidableLE` but
only `Preorder`. -/
def ofIic' (α : Type*) [Preorder α] [DecidableLE α] (finsetIic : α → Finset α)
(mem_Iic : ∀ a x, x ∈ finsetIic a ↔ x ≤ a) : LocallyFiniteOrderBot α
where
finsetIic := finsetIic
finsetIio a := {x ∈ finsetIic a | ¬a ≤ x}
finset_mem_Iic := mem_Iic
finset_mem_Iio a x := by rw [mem_filter, mem_Iic, lt_iff_le_not_ge]
