English
If two subspaces p and q are complementary in E and the complement of {0} is path-connected in p, then the complement of q is path-connected in E.
Русский
Если p и q — попарно дополняющие подпространства в E и дополнение {0} является путепроходимым в p, то дополнение q в E тоже путепроходимо.
LaTeX
$$$ IsPathConnected\ (q^{\complement} : Set\ E) \text{ given } IsPathConnected\ ({0}^{\complement} : Set\ p) \text{ and } IsCompl\ p\ q $$$
Lean4
/-- Given two complementary subspaces `p` and `q` in `E`, if the complement of `{0}`
is path connected in `p` then the complement of `q` is path connected in `E`. -/
theorem isPathConnected_compl_of_isPathConnected_compl_zero {p q : Submodule ℝ E} (hpq : IsCompl p q)
(hpc : IsPathConnected ({0}ᶜ : Set p)) : IsPathConnected (qᶜ : Set E) :=
by
convert (hpc.image continuous_subtype_val).add q.isPathConnected using 1
trans Submodule.prodEquivOfIsCompl p q hpq '' ({0}ᶜ ×ˢ univ)
· rw [prod_univ, LinearEquiv.image_eq_preimage]
ext
simp
· ext
simp [mem_add, and_assoc]
