Theorems · Definition · functional analysis

Submodule.projectionL

{R : Type u_1} →
  [inst : Ring R] →
    {M : Type u_2} →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → (p q : Submodule R M) → Submodule.IsTopCompl p q → M →L[R] M

If h : IsTopCompl p q, h.projection is the continuous linear projection M →L[R] M onto p along q. This is the continuous version of Submodule.IsCompl.projection. See also Submodule.IsTopCompl.projectionOnto for the same projection as an element of M →L[R] p.

Defined in

Mathlib.Topology.Algebra.Module.Complement

Cited by

21 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingTopologicalSpaceAddCommGroupModule