isPreconnected_setOf_sSameSide — Mathlib

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

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