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