case h.e'_6
X : Type u_2
inst✝³ : NormedAddCommGroup X
M : Type u_1
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ P + Q - P * Q = 1 - (1 - P) * (1 - Q)
X : Type u_2
inst✝³ : NormedAddCommGroup X
M : Type u_1
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ IsLprojection X (P + Q - P * Q)
convert (Lcomplement_iff _).mp (h₁.Lcomplement.mul h₂.Lcomplement) using 1
no goals
case h.e'_6
X : Type u_2
inst✝³ : NormedAddCommGroup X
M : Type u_1
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ P + Q - P * Q = 1 - (1 - P) * (1 - Q)
noncomm_ring