case intro
R : Type ?u.503618
V : Type u_1
V' : Type ?u.503624
P : Type u_2
P' : Type ?u.503630
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : ¬x ∈ s
p : P
hp : p ∈ ↑s
⊢ IsConnected {y | SOppSide s x y}
R : Type ?u.503618
V : Type u_1
V' : Type ?u.503624
P : Type u_2
P' : Type ?u.503630
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : ¬x ∈ s
h : Set.Nonempty ↑s
⊢ IsConnected {y | SOppSide s x y}
obtain ⟨p, hp⟩ := h
case intro
R : Type ?u.503618
V : Type u_1
V' : Type ?u.503624
P : Type u_2
P' : Type ?u.503630
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : ¬x ∈ s
p : P
hp : p ∈ ↑s
this : Nonempty { x // x ∈ s }
⊢ IsConnected {y | SOppSide s x y}
case intro
R : Type ?u.503618
V : Type u_1
V' : Type ?u.503624
P : Type u_2
P' : Type ?u.503630
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : ¬x ∈ s
p : P
hp : p ∈ ↑s
⊢ IsConnected {y | SOppSide s x y}
haveI : Nonempty s := ⟨⟨p, hp⟩⟩
case intro
R : Type ?u.503618
V : Type u_1
V' : Type ?u.503624
P : Type u_2
P' : Type ?u.503630
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : ¬x ∈ s
p : P
hp : p ∈ ↑s
this : Nonempty { x // x ∈ s }
⊢ IsConnected ((fun x_1 => x_1.fst • (x -ᵥ p) +ᵥ x_1.snd) '' Set.Iio 0 ×ˢ ↑s)
case intro
R : Type ?u.503618
V : Type u_1
V' : Type ?u.503624
P : Type u_2
P' : Type ?u.503630
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : ¬x ∈ s
p : P
hp : p ∈ ↑s
this : Nonempty { x // x ∈ s }
⊢ IsConnected {y | SOppSide s x y}
rw [setOf_sOppSide_eq_image2 hx hp, ← Set.image_prod]
case intro
R : Type ?u.503618
V : Type u_1
V' : Type ?u.503624
P : Type u_2
P' : Type ?u.503630
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : ¬x ∈ s
p : P
hp : p ∈ ↑s
this : Nonempty { x // x ∈ s }
⊢ ConnectedSpace ↑↑s
case intro
R : Type ?u.503618
V : Type u_1
V' : Type ?u.503624
P : Type u_2
P' : Type ?u.503630
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : ¬x ∈ s
p : P
hp : p ∈ ↑s
this : Nonempty { x // x ∈ s }
⊢ IsConnected ((fun x_1 => x_1.fst • (x -ᵥ p) +ᵥ x_1.snd) '' Set.Iio 0 ×ˢ ↑s)
refine' (isConnected_Iio.prod (isConnected_iff_connectedSpace.2 _)).image _
  ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn
no goals
case intro
R : Type ?u.503618
V : Type u_1
V' : Type ?u.503624
P : Type u_2
P' : Type ?u.503630
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : ¬x ∈ s
p : P
hp : p ∈ ↑s
this : Nonempty { x // x ∈ s }
⊢ ConnectedSpace ↑↑s
convert AddTorsor.connectedSpace s.direction s