English
Let s be an affine subspace and x ∈ P not in s. Then {y | s.SSameSide x y} is preconnected.
Русский
Пусть s — аффинное подпространство и x не принадлежит s. Тогда {y | s.SSameSide x y} предсвязано.
LaTeX
$$$\text{IsPreconnected}\bigl\{y \mid s.SSameSide(x,y)\bigr\}.$$$
Lean4
theorem isPreconnected_setOf_sSameSide (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y | s.SSameSide x y} :=
by
rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)
· rw [coe_eq_bot_iff] at h
simp only [h, not_sSameSide_bot]
exact isPreconnected_empty
· by_cases hx : x ∈ s
· simp only [hx, SSameSide, not_true, false_and, and_false]
exact isPreconnected_empty
· exact (isConnected_setOf_sSameSide hx h).isPreconnected