mem_upperBounds — Mathlib

English

An element a belongs to the set of upper bounds of s if and only if every x in s satisfies x ≤ a.

Русский

Элемент a принадлежит множеству верхних гран s тогда и только тогда, когда для каждого x ∈ s выполняется x ≤ a.

LaTeX

$$$a \\in \\text{upperBounds}(s) \\iff \\forall x \\in s, x \\le a$$$

Lean4

theorem mem_upperBounds : a ∈ upperBounds s ↔ ∀ x ∈ s, x ≤ a :=
  Iff.rfl

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