surjective_comp_subtype_of_isComplemented

English

If p is complemented in E, then the map f ↦ f ∘ p.subtype from E→M to E→M is surjective for linear maps f: E→M.

Русский

Если p дополнено в E, то отображение f ↦ f ∘ p.subtype из E→M в E→M сюръективно.

LaTeX

$$$\text{If } h: IsComplemented(p)\text{, then }(f\mapsto f\circ p.subtype)\colon (E\to M)\to (E\to M)\text{ is surjective}.$$$

Lean4

theorem surjective_comp_subtype_of_isComplemented (h : IsComplemented p) [Module R M] :
    Function.Surjective fun f : E →ₗ[R] M ↦ f ∘ₗ p.subtype :=
  have ⟨q, h⟩ := h;
  fun f ↦ ⟨f ∘ₗ p.linearProjOfIsCompl q h, by ext; simp⟩

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