max_map — Mathlib

English

The pointwise maximum operation on ENormedSpace corresponds to taking the maximum of values.

Русский

Пункто по пункту максимум в ENormedSpace совпадает с максимумом значений.

LaTeX

$$ (e1 ⊔ e2) x = max (e1 x) (e2 x)$$

Lean4

@[deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07"), norm_cast]
theorem max_map (e₁ e₂ : ENormedSpace 𝕜 V) (x : V) : (e₁ ⊔ e₂) x = max (e₁ x) (e₂ x) :=
  rfl

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