English
Let s be an affine subspace of P and x ∈ P such that s is nonempty. Then the set {y | s.SSameSide x y} is connected.
Русский
Пусть s — аффинное подпространство в P и x ∈ P так, что s непусто. Тогда множество {y | s.SSameSide x y} связано.
LaTeX
$$$\text{If } s \text{ is nonempty and } x \in P,\;{y \mid s.SSameSide(x,y)}\text{ is connected.}$$$
Lean4
theorem isConnected_setOf_wSameSide {s : AffineSubspace ℝ P} (x : P) (h : (s : Set P).Nonempty) :
IsConnected {y | s.WSameSide x y} := by
obtain ⟨p, hp⟩ := h
haveI : Nonempty s := ⟨⟨p, hp⟩⟩
by_cases hx : x ∈ s
· simp only [wSameSide_of_left_mem, hx]
have := AddTorsor.connectedSpace V P
exact isConnected_univ
· rw [setOf_wSameSide_eq_image2 hx hp, ← Set.image_prod]
refine
(isConnected_Ici.prod (isConnected_iff_connectedSpace.2 ?_)).image _
((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn
convert AddTorsor.connectedSpace s.direction s
