bddBelow — Mathlib

English

A finite finset is bounded below: there exists a lower bound a with a ≤ x for all x ∈ s.

Русский

Конечный подмножество множества ограничено снизу: существует нижняя граница a такая, что a ≤ x для всех x ∈ s.

LaTeX

$$$\\exists a, \\forall x (x \\in s \\Rightarrow a \\le x)$$$

Lean4

/-- A finset is bounded below. -/
protected theorem bddBelow [SemilatticeInf α] [Nonempty α] (s : Finset α) : BddBelow (↑s : Set α) :=
  s.finite_toSet.bddBelow

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