Theorems · Definition · functional analysis

Submodule.prodEquivOfIsTopCompl

{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) → [IsTopologicalAddGroup M] → Submodule.IsTopCompl p q → (↥p × ↥q) ≃L[R] M

If two submodules are topological complements, then the linear equivalence Submodule.prodEquivOfIsCompl is a homeomorphism, bundled as a continuous linear equivalence.

Defined in

Mathlib.Topology.Algebra.Module.Complement

Cited by

6 results in Mathlib

Foundations

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

Assumes

RingTopologicalSpaceAddCommGroupModuleIsTopologicalAddGroup