postcomp_mkCLM_surjective — Mathlib

English

Postcomposition by mkCLM with respect to f is surjective onto SeparationQuotient E.

Русский

Посткомпозиция mkCLM с f есть сюрьективная относительно SeparationQuotient E.

LaTeX

$$$\text{Surjective}((\mathrm{mkCLM}\ K E) \circ f)$$$

Lean4

theorem postcomp_mkCLM_surjective {L : Type*} [Semiring L] (σ : L →+* K) (F : Type*) [AddCommMonoid F] [Module L F]
    [TopologicalSpace F] : Function.Surjective ((mkCLM K E).comp : (F →SL[σ] E) → (F →SL[σ] SeparationQuotient E)) :=
  by
  intro f
  use (outCLM K E).comp f
  rw [← ContinuousLinearMap.comp_assoc, mkCLM_comp_outCLM, ContinuousLinearMap.id_comp]

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