bddAbove_range_iff — Mathlib

English

For any bounded set of seminorms, the sSup equals the iSup over the coercions; equivalence of sup and pointwise sup.

Русский

Для ограниченного множества семинорм верхняя граница согласуется со свёрткой по точкам.

LaTeX

$$coe_sSup_eq' for bounded sets; equality of sSup and iSup$$

Lean4

protected theorem bddAbove_range_iff {ι : Sort*} {p : ι → Seminorm 𝕜 E} :
    BddAbove (range p) ↔ ∀ x, BddAbove (range fun i ↦ p i x) := by
  rw [Seminorm.bddAbove_iff, ← range_comp, bddAbove_range_pi]; rfl

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