English
There is a canonical supremum for arbitrary sets of seminorms, defined pointwise by suprema of their values where bounded above; if not bounded above, the supremum is set to zero.
Русский
Существует верхняя граница произвольного множества семинорм, задаваемая покоординатно; если множество не ограничено сверху, знак взятия равен нулю.
LaTeX
$$SuppSet s defined by s.sup, with cases depending on boundedness$$
Lean4
theorem smul_inf [SMul R ℝ] [SMul R ℝ≥0] [IsScalarTower R ℝ≥0 ℝ] (r : R) (p q : Seminorm 𝕜 E) :
r • (p ⊓ q) = r • p ⊓ r • q := by
ext
simp_rw [smul_apply, inf_apply, smul_apply, ← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul,
Real.mul_iInf_of_nonneg (NNReal.coe_nonneg _), mul_add]
