bddBelow_def — Mathlib

English

A set s is bounded below if and only if there exists some x such that every y ∈ s satisfies x ≤ y.

Русский

Множество s ограничено снизу тогда и только тогда, когда существует элемент x такой, что для каждого y ∈ s выполняется x ≤ y.

LaTeX

$$$\\text{BddBelow}(s) \\iff \\exists x, \\forall y \\in s, x \\le y$$$

Lean4

theorem bddBelow_def : BddBelow s ↔ ∃ x, ∀ y ∈ s, x ≤ y :=
  Iff.rfl

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