isPreconnected_setOf_wSameSide — Mathlib

English

Let s be an affine subspace of P and x ∈ P. Then the set {y | s.SSameSide x y} is preconnected.

Русский

Пусть s — аффинное подпространство в P и x ∈ P. Тогда множество {y | s.SSameSide x y} предсвязано.

LaTeX

$$$\text{IsPreconnected}\bigl\{y \mid s.SSameSide(x,y)\bigr\}.$$$

Lean4

theorem isPreconnected_setOf_wSameSide (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y | s.WSameSide 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_wSameSide_bot]
    exact isPreconnected_empty
  · exact (isConnected_setOf_wSameSide x h).isPreconnected

Похожие утверждения