finite_of_bddAbove — Mathlib

English

If a set s is bounded below and above in a locally finite order, then s is finite.

Русский

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

LaTeX

$$$BddBelow(s) \\land BddAbove(s) \\Rightarrow s \\text{ finite}$$$

Lean4

theorem finite_of_bddAbove [Preorder α] [LocallyFiniteOrder α] {s : Set α} (h₀ : BddBelow s) (h₁ : BddAbove s) :
    s.Finite :=
  let ⟨a, ha⟩ := h₀
  let ⟨b, hb⟩ := h₁
  (Set.finite_Icc a b).subset fun _x hx ↦ ⟨ha hx, hb hx⟩

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