case intro
R : Type ?u.487918
V : Type u_1
V' : Type ?u.487924
P : Type u_2
P' : Type ?u.487930
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
⊢ IsConnected {y | WOppSide s x y}
R : Type ?u.487918
V : Type u_1
V' : Type ?u.487924
P : Type u_2
P' : Type ?u.487930
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : Set.Nonempty ↑s
⊢ IsConnected {y | WOppSide s x y}
obtain ⟨p, hp⟩ := h
case intro
R : Type ?u.487918
V : Type u_1
V' : Type ?u.487924
P : Type u_2
P' : Type ?u.487930
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this : Nonempty { x // x ∈ s }
⊢ IsConnected {y | WOppSide s x y}
case intro
R : Type ?u.487918
V : Type u_1
V' : Type ?u.487924
P : Type u_2
P' : Type ?u.487930
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
⊢ IsConnected {y | WOppSide s x y}
haveI : Nonempty s := ⟨⟨p, hp⟩⟩
case pos
R : Type ?u.487918
V : Type u_1
V' : Type ?u.487924
P : Type u_2
P' : Type ?u.487930
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this : Nonempty { x // x ∈ s }
hx : x ∈ s
⊢ IsConnected {y | WOppSide s x y}

case neg
R : Type ?u.487918
V : Type u_1
V' : Type ?u.487924
P : Type u_2
P' : Type ?u.487930
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this : Nonempty { x // x ∈ s }
hx : ¬x ∈ s
⊢ IsConnected {y | WOppSide s x y}
case intro
R : Type ?u.487918
V : Type u_1
V' : Type ?u.487924
P : Type u_2
P' : Type ?u.487930
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this : Nonempty { x // x ∈ s }
⊢ IsConnected {y | WOppSide s x y}
by_cases hx : x ∈ s
case pos
R : Type ?u.487918
V : Type u_1
V' : Type ?u.487924
P : Type u_2
P' : Type ?u.487930
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this : Nonempty { x // x ∈ s }
hx : x ∈ s
⊢ IsConnected {y | True}
case pos
R : Type ?u.487918
V : Type u_1
V' : Type ?u.487924
P : Type u_2
P' : Type ?u.487930
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this : Nonempty { x // x ∈ s }
hx : x ∈ s
⊢ IsConnected {y | WOppSide s x y}
simp only [wOppSide_of_left_mem, hx]
case pos
R : Type ?u.487918
V : Type u_1
V' : Type ?u.487924
P : Type u_2
P' : Type ?u.487930
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this✝ : Nonempty { x // x ∈ s }
hx : x ∈ s
this : ConnectedSpace P
⊢ IsConnected {y | True}
case pos
R : Type ?u.487918
V : Type u_1
V' : Type ?u.487924
P : Type u_2
P' : Type ?u.487930
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this : Nonempty { x // x ∈ s }
hx : x ∈ s
⊢ IsConnected {y | True}
have := AddTorsor.connectedSpace V P
no goals
case pos
R : Type ?u.487918
V : Type u_1
V' : Type ?u.487924
P : Type u_2
P' : Type ?u.487930
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this✝ : Nonempty { x // x ∈ s }
hx : x ∈ s
this : ConnectedSpace P
⊢ IsConnected {y | True}
exact isConnected_univ
case neg
R : Type ?u.487918
V : Type u_1
V' : Type ?u.487924
P : Type u_2
P' : Type ?u.487930
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this : Nonempty { x // x ∈ s }
hx : ¬x ∈ s
⊢ IsConnected ((fun x_1 => x_1.fst • (x -ᵥ p) +ᵥ x_1.snd) '' Set.Iic 0 ×ˢ ↑s)
case neg
R : Type ?u.487918
V : Type u_1
V' : Type ?u.487924
P : Type u_2
P' : Type ?u.487930
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this : Nonempty { x // x ∈ s }
hx : ¬x ∈ s
⊢ IsConnected {y | WOppSide s x y}
rw [setOf_wOppSide_eq_image2 hx hp, ← Set.image_prod]
case neg
R : Type ?u.487918
V : Type u_1
V' : Type ?u.487924
P : Type u_2
P' : Type ?u.487930
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this : Nonempty { x // x ∈ s }
hx : ¬x ∈ s
⊢ ConnectedSpace ↑↑s
case neg
R : Type ?u.487918
V : Type u_1
V' : Type ?u.487924
P : Type u_2
P' : Type ?u.487930
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this : Nonempty { x // x ∈ s }
hx : ¬x ∈ s
⊢ IsConnected ((fun x_1 => x_1.fst • (x -ᵥ p) +ᵥ x_1.snd) '' Set.Iic 0 ×ˢ ↑s)
refine' (isConnected_Iic.prod (isConnected_iff_connectedSpace.2 _)).image _
  ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn
no goals
case neg
R : Type ?u.487918
V : Type u_1
V' : Type ?u.487924
P : Type u_2
P' : Type ?u.487930
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this : Nonempty { x // x ∈ s }
hx : ¬x ∈ s
⊢ ConnectedSpace ↑↑s
convert AddTorsor.connectedSpace s.direction s