[GOAL]
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
x : E
x✝² : x ∈ s
y : E
x✝¹ : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : a + b = 1
⊢ ‖a • x‖ + ‖b • y‖ = a * ‖x‖ + b * ‖y‖
[PROOFSTEP]
rw [norm_smul, norm_smul, Real.norm_of_nonneg ha, Real.norm_of_nonneg hb]
[GOAL]
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
z : E
hs : Convex ℝ s
⊢ ConvexOn ℝ s fun z' => dist z' z
[PROOFSTEP]
simpa [dist_eq_norm, preimage_preimage] using
  (convexOn_norm (hs.translate (-z))).comp_affineMap (AffineMap.id ℝ E - AffineMap.const ℝ E z)
[GOAL]
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
a : E
r : ℝ
⊢ Convex ℝ (ball a r)
[PROOFSTEP]
simpa only [Metric.ball, sep_univ] using (convexOn_univ_dist a).convex_lt r
[GOAL]
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
a : E
r : ℝ
⊢ Convex ℝ (closedBall a r)
[PROOFSTEP]
simpa only [Metric.closedBall, sep_univ] using (convexOn_univ_dist a).convex_le r
[GOAL]
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
δ : ℝ
⊢ Convex ℝ (Metric.thickening δ s)
[PROOFSTEP]
rw [← add_ball_zero]
[GOAL]
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
δ : ℝ
⊢ Convex ℝ (s + ball 0 δ)
[PROOFSTEP]
exact hs.add (convex_ball 0 _)
[GOAL]
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
δ : ℝ
⊢ Convex ℝ (Metric.cthickening δ s)
[PROOFSTEP]
obtain hδ | hδ := le_total 0 δ
[GOAL]
case inl
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
δ : ℝ
hδ : 0 ≤ δ
⊢ Convex ℝ (Metric.cthickening δ s)
[PROOFSTEP]
rw [cthickening_eq_iInter_thickening hδ]
[GOAL]
case inl
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
δ : ℝ
hδ : 0 ≤ δ
⊢ Convex ℝ (⋂ (ε : ℝ) (_ : δ < ε), Metric.thickening ε s)
[PROOFSTEP]
exact convex_iInter₂ fun _ _ => hs.thickening _
[GOAL]
case inr
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
δ : ℝ
hδ : δ ≤ 0
⊢ Convex ℝ (Metric.cthickening δ s)
[PROOFSTEP]
rw [cthickening_of_nonpos hδ]
[GOAL]
case inr
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
δ : ℝ
hδ : δ ≤ 0
⊢ Convex ℝ (closure s)
[PROOFSTEP]
exact hs.closure
[GOAL]
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t✝ s t : Set E
x y : E
hx : x ∈ ↑(convexHull ℝ) s
hy : y ∈ ↑(convexHull ℝ) t
⊢ ∃ x', x' ∈ s ∧ ∃ y', y' ∈ t ∧ dist x y ≤ dist x' y'
[PROOFSTEP]
rcases convexHull_exists_dist_ge hx y with ⟨x', hx', Hx'⟩
[GOAL]
case intro.intro
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t✝ s t : Set E
x y : E
hx : x ∈ ↑(convexHull ℝ) s
hy : y ∈ ↑(convexHull ℝ) t
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
⊢ ∃ x', x' ∈ s ∧ ∃ y', y' ∈ t ∧ dist x y ≤ dist x' y'
[PROOFSTEP]
rcases convexHull_exists_dist_ge hy x' with ⟨y', hy', Hy'⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t✝ s t : Set E
x y : E
hx : x ∈ ↑(convexHull ℝ) s
hy : y ∈ ↑(convexHull ℝ) t
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
y' : E
hy' : y' ∈ t
Hy' : dist y x' ≤ dist y' x'
⊢ ∃ x', x' ∈ s ∧ ∃ y', y' ∈ t ∧ dist x y ≤ dist x' y'
[PROOFSTEP]
use x', hx', y', hy'
[GOAL]
case right
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t✝ s t : Set E
x y : E
hx : x ∈ ↑(convexHull ℝ) s
hy : y ∈ ↑(convexHull ℝ) t
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
y' : E
hy' : y' ∈ t
Hy' : dist y x' ≤ dist y' x'
⊢ dist x y ≤ dist x' y'
[PROOFSTEP]
exact le_trans Hx' (dist_comm y x' ▸ dist_comm y' x' ▸ Hy')
[GOAL]
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
⊢ EMetric.diam (↑(convexHull ℝ) s) = EMetric.diam s
[PROOFSTEP]
refine' (EMetric.diam_le fun x hx y hy => _).antisymm (EMetric.diam_mono <| subset_convexHull ℝ s)
[GOAL]
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
x : E
hx : x ∈ ↑(convexHull ℝ) s
y : E
hy : y ∈ ↑(convexHull ℝ) s
⊢ edist x y ≤ EMetric.diam s
[PROOFSTEP]
rcases convexHull_exists_dist_ge2 hx hy with ⟨x', hx', y', hy', H⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
x : E
hx : x ∈ ↑(convexHull ℝ) s
y : E
hy : y ∈ ↑(convexHull ℝ) s
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ edist x y ≤ EMetric.diam s
[PROOFSTEP]
rw [edist_dist]
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
x : E
hx : x ∈ ↑(convexHull ℝ) s
y : E
hy : y ∈ ↑(convexHull ℝ) s
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ ENNReal.ofReal (dist x y) ≤ EMetric.diam s
[PROOFSTEP]
apply le_trans (ENNReal.ofReal_le_ofReal H)
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
x : E
hx : x ∈ ↑(convexHull ℝ) s
y : E
hy : y ∈ ↑(convexHull ℝ) s
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ ENNReal.ofReal (dist x' y') ≤ EMetric.diam s
[PROOFSTEP]
rw [← edist_dist]
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
x : E
hx : x ∈ ↑(convexHull ℝ) s
y : E
hy : y ∈ ↑(convexHull ℝ) s
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ edist x' y' ≤ EMetric.diam s
[PROOFSTEP]
exact EMetric.edist_le_diam_of_mem hx' hy'
[GOAL]
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
⊢ diam (↑(convexHull ℝ) s) = diam s
[PROOFSTEP]
simp only [Metric.diam, convexHull_ediam]
[GOAL]
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
⊢ Metric.Bounded (↑(convexHull ℝ) s) ↔ Metric.Bounded s
[PROOFSTEP]
simp only [Metric.bounded_iff_ediam_ne_top, convexHull_ediam]
[GOAL]
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x : E
r : ℝ
r_pos : 0 < r
⊢ Set.Nonempty (ball x r)
[PROOFSTEP]
simp [r_pos]
[GOAL]
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x y z : E
h : y ∈ [x-[ℝ]z]
⊢ dist x y + dist y z = dist x z
[PROOFSTEP]
simp only [dist_eq_norm, mem_segment_iff_sameRay] at *
[GOAL]
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x y z : E
h : SameRay ℝ (y - x) (z - y)
⊢ ‖x - y‖ + ‖y - z‖ = ‖x - z‖
[PROOFSTEP]
simpa only [sub_add_sub_cancel', norm_sub_rev] using h.norm_add.symm
[GOAL]
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x : E
⊢ IsConnected {y | SameRay ℝ x y}
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x : E
hx : x = 0
⊢ IsConnected {y | SameRay ℝ x y}
[PROOFSTEP]
simpa [hx] using isConnected_univ (α := E)
[GOAL]
case neg
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x : E
hx : ¬x = 0
⊢ IsConnected {y | SameRay ℝ x y}
[PROOFSTEP]
simp_rw [← exists_nonneg_left_iff_sameRay hx]
[GOAL]
case neg
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x : E
hx : ¬x = 0
⊢ IsConnected {y | ∃ r, 0 ≤ r ∧ r • x = y}
[PROOFSTEP]
exact isConnected_Ici.image _ (continuous_id.smul continuous_const).continuousOn
[GOAL]
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x : E
hx : x ≠ 0
⊢ IsConnected {y | SameRay ℝ x y ∧ y ≠ 0}
[PROOFSTEP]
simp_rw [← exists_pos_left_iff_sameRay_and_ne_zero hx]
[GOAL]
ι : Type u_1
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
x : E
hx : x ≠ 0
⊢ IsConnected {y | ∃ r, 0 < r ∧ r • x = y}
[PROOFSTEP]
exact isConnected_Ioi.image _ (continuous_id.smul continuous_const).continuousOn
