isConnected_setOf_sSameSide — Mathlib

English

Let s be an affine subspace and x ∈ P with s ≠ ∅. Then the set {y | s.SSameSide x y} is connected.

Русский

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

LaTeX

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

Lean4

theorem isConnected_setOf_sSameSide {s : AffineSubspace ℝ P} {x : P} (hx : x ∉ s) (h : (s : Set P).Nonempty) :
    IsConnected {y | s.SSameSide x y} := by
  obtain ⟨p, hp⟩ := h
  haveI : Nonempty s := ⟨⟨p, hp⟩⟩
  rw [setOf_sSameSide_eq_image2 hx hp, ← Set.image_prod]
  refine
    (isConnected_Ioi.prod (isConnected_iff_connectedSpace.2 ?_)).image _
      ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn
  convert AddTorsor.connectedSpace s.direction s

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