Theorems · Theorem · functional analysis

ClosedSubmodule.orthogonal_disjoint

∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : ClosedSubmodule 𝕜 E), Disjoint K Kᗮ

K and Kᗮ have trivial intersection.

Defined in: Mathlib.Analysis.InnerProductSpace.Orthogonal
Cited by: 1 results in Mathlib
Foundations: Depth 184 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: RCLike NormedAddCommGroup InnerProductSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites8

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

NormedAddCommGroupstatement and proof · cited by 15,752
Bot.botproof · cited by 4,720
InnerProductSpacestatement and proof · cited by 3,523
RCLikestatement and proof · cited by 2,829
Disjointstatement · cited by 2,201
ClosedSubmodulestatement and proof · cited by 123
ClosedSubmodule.orthogonalstatement · cited by 32
ClosedSubmodule.inf_orthogonal_eq_botproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

ClosedSubmodule.orthogonal_eq_top_iffproof · cited by 0