bddAbove_def — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem bddAbove_def : BddAbove s ↔ ∃ x, ∀ y ∈ s, y ≤ x :=
  Iff.rfl

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