Theorems · Theorem · functional analysis
IsLprojection.Lcomplement
∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X] {P : M},
IsLprojection X P → IsLprojection X (1 - P)- Cited by
- 3 results in Mathlib
- Foundations
- Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NormedAddCommGroupRingModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realproof · cited by 25,697
- Modulestatement and proof · cited by 20,661
- NormedAddCommGroupstatement and proof · cited by 15,752
- Ringstatement and proof · cited by 7,463
- Norm.normproof · cited by 5,413
- add_commproof · cited by 1,535
- sub_sub_cancelproof · cited by 105
- IsIdempotentElem.one_subproof · cited by 20
- IsLprojectionstatement and proof · cited by 19
- IsLprojection.projproof · cited by 5
- IsLprojection.Lnormproof · cited by 3
Cited by3
Results whose statement or proof uses this declaration.
- IsLprojection.commuteproof · cited by 2
- IsLprojection.Lcomplement_iffproof · cited by 1
- IsLprojection.joinproof · cited by 0