ext — Mathlib

English

If two compactly supported continuous maps f and g from α to β agree at every point x ∈ α, then f and g are equal as elements of C_c(α, β).

Русский

Если две компактно поддерживаемые непрерывные отображения f и g из α в β совпадают при каждой точке x ∈ α, то они равны в C_c(α, β).

LaTeX

$$$ \forall f,g : C_c(α, β), \big( \forall x, f(x) = g(x) \big) \Rightarrow f = g $$$

Lean4

@[ext]
theorem ext {f g : C_c(α, β)} (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext _ _ h

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