English
In a nonempty lattice with LocallyFiniteOrder, a set s is finite exactly when it is both bounded below and bounded above.
Русский
В ненулевом решении порядке с локально конечным порядком множество конечное тогда и только тогда, когда оно ограничено снизу и сверху.
LaTeX
$$$s \\text{ finite} \\iff (BddBelow(s) \\land BddAbove(s))$$$
Lean4
theorem finite_iff_bddBelow_bddAbove [Nonempty α] [Lattice α] [LocallyFiniteOrder α] :
s.Finite ↔ BddBelow s ∧ BddAbove s :=
by
obtain (rfl | hs) := s.eq_empty_or_nonempty
· simp only [Set.finite_empty, bddBelow_empty, bddAbove_empty, and_self]
exact
⟨fun h ↦
⟨⟨h.toFinset.inf' ((Finite.toFinset_nonempty h).mpr hs) id, fun x hx ↦
Finset.inf'_le id ((Finite.mem_toFinset h).mpr hx)⟩,
⟨h.toFinset.sup' ((Finite.toFinset_nonempty h).mpr hs) id, fun x hx ↦
Finset.le_sup' id ((Finite.mem_toFinset h).mpr hx)⟩⟩,
fun ⟨h₀, h₁⟩ ↦ BddBelow.finite_of_bddAbove h₀ h₁⟩
