surjective_comp_linearProjOfIsCompl

English

The range (image) of the glued map is the sup of the ranges of φ and ψ.

Русский

Образ слитого отображения равен сумме образов φ и ψ.

LaTeX

$$$\operatorname{range}(\mathrm{ofIsCompl}\ h\ φ\ ψ) = \operatorname{range}(φ) \sqcup \operatorname{range}(ψ).$$$

Lean4

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

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