case inl
R : Type ?u.470015
V : Type u_1
V' : Type ?u.470021
P : Type u_2
P' : Type ?u.470027
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : ↑s = ∅
⊢ IsPreconnected {y | WSameSide s x y}

case inr
R : Type ?u.470015
V : Type u_1
V' : Type ?u.470021
P : Type u_2
P' : Type ?u.470027
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : Set.Nonempty ↑s
⊢ IsPreconnected {y | WSameSide s x y}
R : Type ?u.470015
V : Type u_1
V' : Type ?u.470021
P : Type u_2
P' : Type ?u.470027
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
⊢ IsPreconnected {y | WSameSide s x y}
rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)
case inl
R : Type ?u.470015
V : Type u_1
V' : Type ?u.470021
P : Type u_2
P' : Type ?u.470027
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
⊢ IsPreconnected {y | WSameSide s x y}
case inl
R : Type ?u.470015
V : Type u_1
V' : Type ?u.470021
P : Type u_2
P' : Type ?u.470027
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : ↑s = ∅
⊢ IsPreconnected {y | WSameSide s x y}
rw [coe_eq_bot_iff] at h
case inl
R : Type ?u.470015
V : Type u_1
V' : Type ?u.470021
P : Type u_2
P' : Type ?u.470027
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
⊢ IsPreconnected {y | False}
case inl
R : Type ?u.470015
V : Type u_1
V' : Type ?u.470021
P : Type u_2
P' : Type ?u.470027
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
⊢ IsPreconnected {y | WSameSide s x y}
simp only [h, not_wSameSide_bot]
no goals
case inl
R : Type ?u.470015
V : Type u_1
V' : Type ?u.470021
P : Type u_2
P' : Type ?u.470027
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
⊢ IsPreconnected {y | False}
exact isPreconnected_empty
no goals
case inr
R : Type ?u.470015
V : Type u_1
V' : Type ?u.470021
P : Type u_2
P' : Type ?u.470027
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : Set.Nonempty ↑s
⊢ IsPreconnected {y | WSameSide s x y}
exact (isConnected_setOf_wSameSide x h).isPreconnected