sSup_empty — Mathlib

English

The supremum of the empty collection of seminorms is the bottom element of the lattice of seminorms: sSup(∅) = ⊥.

Русский

Супремум пустого множества семинорм равен нижнему элементу задающейся на нем решетки: sSup(∅) = ⊥.

LaTeX

$$$\\mathrm{sSup}(\\emptyset) = \\bot$$$

Lean4

protected theorem sSup_empty : sSup (∅ : Set (Seminorm 𝕜 E)) = ⊥ :=
  by
  ext
  rw [Seminorm.sSup_apply bddAbove_empty, Real.iSup_of_isEmpty]
  rfl

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