English
A variant of LocallyFiniteOrderBot built from Iic, with finsetIio defined via x ≠ a and mem_Iic ensuring x ≤ a.
Русский
Вариант LocallyFiniteOrderBot из Iic, где finsetIio определяется как x ≠ a, а принадлежность задаётся x ≤ a.
LaTeX
$$$\mathrm{LocallyFiniteOrderBot}(\alpha) := \text{финсет из }finsetIic \text{ с }finsetIio(a) = \{x \in finsetIic(a) \mid x \neq 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 `PartialOrder` but
only `DecidableEq`. -/
def ofIic (α : Type*) [PartialOrder α] [DecidableEq α] (finsetIic : α → Finset α)
(mem_Iic : ∀ a x, x ∈ finsetIic a ↔ x ≤ a) : LocallyFiniteOrderBot α
where
finsetIic := finsetIic
finsetIio a := {x ∈ finsetIic a | x ≠ a}
finset_mem_Iic := mem_Iic
finset_mem_Iio a x := by rw [mem_filter, mem_Iic, lt_iff_le_and_ne]
