isConnected_setOf_sOppSide — Mathlib

English

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

Русский

Пусть s — аффинное подпространство и x ∉ s. Тогда {y | s.SOppSide x y} связано.

LaTeX

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

Lean4

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

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