ι : Type ?u.38573
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
x : E
hx : x ∈ ↑(convexHull ℝ).toOrderHom s
y : E
hy : y ∈ ↑(convexHull ℝ).toOrderHom s
⊢ edist x y ≤ EMetric.diam s
ι : Type ?u.38573
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
⊢ EMetric.diam (↑(convexHull ℝ).toOrderHom s) = EMetric.diam s
refine' (EMetric.diam_le fun x hx y hy => _).antisymm (EMetric.diam_mono <| subset_convexHull ℝ s)
case intro.intro.intro.intro
ι : Type ?u.38573
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
x : E
hx : x ∈ ↑(convexHull ℝ).toOrderHom s
y : E
hy : y ∈ ↑(convexHull ℝ).toOrderHom s
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ edist x y ≤ EMetric.diam s
ι : Type ?u.38573
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
x : E
hx : x ∈ ↑(convexHull ℝ).toOrderHom s
y : E
hy : y ∈ ↑(convexHull ℝ).toOrderHom s
⊢ edist x y ≤ EMetric.diam s
rcases convexHull_exists_dist_ge2 hx hy with ⟨x', hx', y', hy', H⟩
case intro.intro.intro.intro
ι : Type ?u.38573
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
x : E
hx : x ∈ ↑(convexHull ℝ).toOrderHom s
y : E
hy : y ∈ ↑(convexHull ℝ).toOrderHom 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
case intro.intro.intro.intro
ι : Type ?u.38573
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
x : E
hx : x ∈ ↑(convexHull ℝ).toOrderHom s
y : E
hy : y ∈ ↑(convexHull ℝ).toOrderHom s
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ edist x y ≤ EMetric.diam s
rw [edist_dist]
case intro.intro.intro.intro
ι : Type ?u.38573
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
x : E
hx : x ∈ ↑(convexHull ℝ).toOrderHom s
y : E
hy : y ∈ ↑(convexHull ℝ).toOrderHom 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
case intro.intro.intro.intro
ι : Type ?u.38573
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
x : E
hx : x ∈ ↑(convexHull ℝ).toOrderHom s
y : E
hy : y ∈ ↑(convexHull ℝ).toOrderHom 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
apply le_trans (ENNReal.ofReal_le_ofReal H)
case intro.intro.intro.intro
ι : Type ?u.38573
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
x : E
hx : x ∈ ↑(convexHull ℝ).toOrderHom s
y : E
hy : y ∈ ↑(convexHull ℝ).toOrderHom s
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ edist x' y' ≤ EMetric.diam s
case intro.intro.intro.intro
ι : Type ?u.38573
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
x : E
hx : x ∈ ↑(convexHull ℝ).toOrderHom s
y : E
hy : y ∈ ↑(convexHull ℝ).toOrderHom 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
rw [← edist_dist]
no goals
case intro.intro.intro.intro
ι : Type ?u.38573
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s✝ t s : Set E
x : E
hx : x ∈ ↑(convexHull ℝ).toOrderHom s
y : E
hy : y ∈ ↑(convexHull ℝ).toOrderHom s
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ edist x' y' ≤ EMetric.diam s
exact EMetric.edist_le_diam_of_mem hx' hy'