finite_iff_bddAbove — Mathlib

English

In a semilattice with a locally finite order and a bottom element, a subset s is finite exactly when it is bounded above.

Русский

В полупорядованном множестве с нижней гранью и локально конечным порядком множество s конечное тогда и только тогда, когда оно ограничено сверху.

LaTeX

$$$s^{-} \\text{ finite} \\iff BddAbove(s)$$$

Lean4

theorem finite_iff_bddAbove [SemilatticeSup α] [LocallyFiniteOrder α] [OrderBot α] : s.Finite ↔ BddAbove s :=
  ⟨fun h ↦ ⟨h.toFinset.sup id, fun _ hx ↦ Finset.le_sup (f := id) ((Finite.mem_toFinset h).mpr hx)⟩, fun ⟨m, hm⟩ ↦
    (Set.finite_Icc ⊥ m).subset (fun _ hx ↦ ⟨bot_le, hm hx⟩)⟩

Похожие утверждения