to_continuousMap_injective — Mathlib

English

The forgetful map from ContinuousAffineMap to ContinuousMap is injective.

Русский

Отображение забывания из ContinuousAffineMap в ContinuousMap инъективно.

LaTeX

$$$@\text{theorem } to_continuousMap_injective {f g : P \toᴬ[R] Q} (h : (f : C(P, Q)) = (g : C(P, Q))) : f = g$$$

Lean4

theorem to_continuousMap_injective {f g : P →ᴬ[R] Q} (h : (f : C(P, Q)) = (g : C(P, Q))) : f = g :=
  by
  ext a
  exact ContinuousMap.congr_fun h a

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