coe_max — Mathlib

English

Provide max operator coherence with pointwise order and maps.

Русский

Обеспечение согласованности максимума с точечным порядком и отображениями.

LaTeX

$$∀ e1 e2 x, max(e1 x, e2 x) = (max e1 e2) x$$

Lean4

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

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