finite_iff_bddBelow — Mathlib

English

Dually, in the dual order, a set is finite iff it is bounded below.

Русский

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

LaTeX

$$$s \\text{ finite in } \\alpha \\iff BddBelow(s)\\text{ in } \\alpha^{\\mathrm{op}}$$$

Lean4

theorem finite_iff_bddBelow [SemilatticeInf α] [LocallyFiniteOrder α] [OrderTop α] : s.Finite ↔ BddBelow s :=
  finite_iff_bddAbove (α := αᵒᵈ)

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