coe_sup — Mathlib

English

The function underlying the supremum of two seminorms is the pointwise maximum of their underlying functions: (p ⊔ q)(x) = max(p(x), q(x)).

Русский

Функция, лежащая в основе наибольшего из двух семинорм, равна точечному максимуму их функций: (p ⊔ q)(x) = max(p(x), q(x)).

LaTeX

$$$ (p \sqcup q)(x) = \max\{ p(x), q(x) \} $ for all x ∈ E$$

Lean4

@[simp, norm_cast]
theorem coe_sup : ⇑(p ⊔ q) = ⇑p ⊔ ⇑q :=
  rfl

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