English
Let p and q be complementary subspaces of E with h the complement isomorphism. Then for every x ∈ E, the second coordinate of the inverse image of x under prodEquivOfIsCompl is 0 if and only if x ∈ p.
Русский
Пусть p и q — комплементарные подпространства E и пусть h — изоморфизм дополнения. Тогда для любого x ∈ E вторая компонента образа x через обратное отображение разложения x = u + v, с u ∈ p, v ∈ q, равна 0 тогда и только тогда, когда x ∈ p.
LaTeX
$$$\forall x \in E,\; \operatorname{snd}\bigl((\mathrm{prodEquivOfIsCompl}\,p\,q\,h)^{-1}(x)\bigr)=0 \iff x \in p$$$
Lean4
@[simp]
theorem prodEquivOfIsCompl_symm_apply_snd_eq_zero (h : IsCompl p q) {x : E} :
((prodEquivOfIsCompl p q h).symm x).2 = 0 ↔ x ∈ p :=
by
conv_rhs => rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]
rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_right _ (Submodule.coe_mem _),
mem_left_iff_eq_zero_of_disjoint h.disjoint]
