coe_continuousMap_mk — Mathlib

English

There is an injectivity statement for the map from ContinuousAffineMap to ContinuousMap in another formulation.

Русский

Существует другое формулирование утверждения инъективности отображения из ContinuousAffineMap в ContinuousMap.

LaTeX

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

Lean4

@[norm_cast]
theorem coe_continuousMap_mk (f : P →ᵃ[R] Q) (h) : ((⟨f, h⟩ : P →ᴬ[R] Q) : C(P, Q)) = ⟨f, h⟩ :=
  rfl

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