bddBelow — Mathlib

English

Let α be a preorder directed by ≥ and nonempty. Then every finite subset s ⊆ α has a lower bound.

Русский

Пусть α — множество с предикатом порядка и направлено снизу относительно ≥, и оно непусто. Тогда любая конечная подмножество s ⊆ α имеет нижнюю границу.

LaTeX

$$$\\exists a \\in \\alpha\\, \\forall x \\in s, a \\le x$$$

Lean4

/-- A finite set is bounded below. -/
protected theorem bddBelow (hs : s.Finite) : BddBelow s :=
  Finite.bddAbove (α := αᵒᵈ) hs

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