ext — Mathlib

English

If two extended-normed spaces have the same action on all vectors, they are equal.

Русский

Если два расширенных нормированных пространства одинаково действуют на все вектора, они равны.

LaTeX

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

Lean4

@[deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07"), ext]
theorem ext {e₁ e₂ : ENormedSpace 𝕜 V} (h : ∀ x, e₁ x = e₂ x) : e₁ = e₂ :=
  coeFn_injective <| funext h

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