Theorems · Theorem · functional analysis

Submodule.continuous_prodEquivOfIsCompl

∀ {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] (h : IsCompl p q),
  Continuous ⇑(p.prodEquivOfIsCompl q h)

The linear equivalence Submodule.prodEquivOfIsCompl from a pair of complementary submodules is always continuous.

Defined in: Mathlib.Topology.Algebra.Module.Complement
Cited by: 2 results in Mathlib
Foundations: Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Ring TopologicalSpace AddCommGroup Module IsTopologicalAddGroup

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites17

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement · cited by 62,936
TopologicalSpacestatement and proof · cited by 24,529
Modulestatement and proof · cited by 20,661
RingHom.idstatement · cited by 18,349
AddCommGroupstatement and proof · cited by 12,871
Ringstatement and proof · cited by 7,463
Submodulestatement and proof · cited by 7,192
LinearEquivstatement · cited by 3,317
Continuousstatement · cited by 2,592
IsTopologicalAddGroupstatement and proof · cited by 1,394
Continuous.compproof · cited by 371
IsComplstatement and proof · cited by 351

Cited by2

Results whose statement or proof uses this declaration.

Submodule.IsCompl.isTopCompl_of_isClosedproof · cited by 2
Submodule.IsCompl.isTopCompl_iff_isHomeomorph_prodEquivOfIsComplproof · cited by 0