upperBounds_eq — Mathlib

English

If h is IsLUB s a, then upperBounds s = Ici a.

Русский

Если a является наибольшей верхней границей множества s, то верхние границы s равны множеству {x | a ≤ x}.

LaTeX

$$∀ {s a}, IsLUB s a → \operatorname{upperBounds}(s) = \{ x \mid a \le x \} = \operatorname{Ici}(a)$$

Lean4

theorem upperBounds_eq (h : IsLUB s a) : upperBounds s = Ici a :=
  Set.ext fun _ => ⟨fun hb => h.2 hb, fun hb => upperBounds_mono_mem hb h.1⟩

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