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

case inr
R : Type ?u.485293
V : Type u_1
V' : Type ?u.485299
P : Type u_2
P' : Type ?u.485305
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : Set.Nonempty ↑s
⊢ IsPreconnected {y | SSameSide s x y}
R : Type ?u.485293
V : Type u_1
V' : Type ?u.485299
P : Type u_2
P' : Type ?u.485305
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
⊢ IsPreconnected {y | SSameSide s x y}
rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)
case inl
R : Type ?u.485293
V : Type u_1
V' : Type ?u.485299
P : Type u_2
P' : Type ?u.485305
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
⊢ IsPreconnected {y | SSameSide s x y}
case inl
R : Type ?u.485293
V : Type u_1
V' : Type ?u.485299
P : Type u_2
P' : Type ?u.485305
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : ↑s = ∅
⊢ IsPreconnected {y | SSameSide s x y}
rw [coe_eq_bot_iff] at h
case inl
R : Type ?u.485293
V : Type u_1
V' : Type ?u.485299
P : Type u_2
P' : Type ?u.485305
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.485293
V : Type u_1
V' : Type ?u.485299
P : Type u_2
P' : Type ?u.485305
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
⊢ IsPreconnected {y | SSameSide s x y}
simp only [h, not_sSameSide_bot]
no goals
case inl
R : Type ?u.485293
V : Type u_1
V' : Type ?u.485299
P : Type u_2
P' : Type ?u.485305
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
case pos
R : Type ?u.485293
V : Type u_1
V' : Type ?u.485299
P : Type u_2
P' : Type ?u.485305
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : Set.Nonempty ↑s
hx : x ∈ s
⊢ IsPreconnected {y | SSameSide s x y}

case neg
R : Type ?u.485293
V : Type u_1
V' : Type ?u.485299
P : Type u_2
P' : Type ?u.485305
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : Set.Nonempty ↑s
hx : ¬x ∈ s
⊢ IsPreconnected {y | SSameSide s x y}
case inr
R : Type ?u.485293
V : Type u_1
V' : Type ?u.485299
P : Type u_2
P' : Type ?u.485305
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : Set.Nonempty ↑s
⊢ IsPreconnected {y | SSameSide s x y}
by_cases hx : x ∈ s
case pos
R : Type ?u.485293
V : Type u_1
V' : Type ?u.485299
P : Type u_2
P' : Type ?u.485305
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : Set.Nonempty ↑s
hx : x ∈ s
⊢ IsPreconnected {y | False}
case pos
R : Type ?u.485293
V : Type u_1
V' : Type ?u.485299
P : Type u_2
P' : Type ?u.485305
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : Set.Nonempty ↑s
hx : x ∈ s
⊢ IsPreconnected {y | SSameSide s x y}
simp only [hx, SSameSide, not_true, false_and_iff, and_false_iff]
no goals
case pos
R : Type ?u.485293
V : Type u_1
V' : Type ?u.485299
P : Type u_2
P' : Type ?u.485305
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : Set.Nonempty ↑s
hx : x ∈ s
⊢ IsPreconnected {y | False}
exact isPreconnected_empty
no goals
case neg
R : Type ?u.485293
V : Type u_1
V' : Type ?u.485299
P : Type u_2
P' : Type ?u.485305
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : Set.Nonempty ↑s
hx : ¬x ∈ s
⊢ IsPreconnected {y | SSameSide s x y}
exact (isConnected_setOf_sSameSide hx h).isPreconnected