[GOAL]
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsLocalMinOn f (Icc a b) a
h_conv : ConvexOn ℝ (Icc a b) f
⊢ IsMinOn f (Icc a b) a
[PROOFSTEP]
rintro c hc
[GOAL]
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsLocalMinOn f (Icc a b) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
⊢ c ∈ {x | (fun x => f a ≤ f x) x}
[PROOFSTEP]
dsimp only [mem_setOf_eq]
[GOAL]
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsLocalMinOn f (Icc a b) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
⊢ f a ≤ f c
[PROOFSTEP]
rw [IsLocalMinOn, nhdsWithin_Icc_eq_nhdsWithin_Ici a_lt_b] at h_local_min
[GOAL]
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[Ici a] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
⊢ f a ≤ f c
[PROOFSTEP]
rcases hc.1.eq_or_lt with (rfl | a_lt_c)
[GOAL]
case inl
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[Ici a] a) a
h_conv : ConvexOn ℝ (Icc a b) f
hc : a ∈ Icc a b
⊢ f a ≤ f a
[PROOFSTEP]
exact le_rfl
[GOAL]
case inr
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[Ici a] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
⊢ f a ≤ f c
[PROOFSTEP]
have H₁ : ∀ᶠ y in 𝓝[>] a, f a ≤ f y := h_local_min.filter_mono (nhdsWithin_mono _ Ioi_subset_Ici_self)
[GOAL]
case inr
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[Ici a] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[Ioi a] a, f a ≤ f y
⊢ f a ≤ f c
[PROOFSTEP]
have H₂ : ∀ᶠ y in 𝓝[>] a, y ∈ Ioc a c := Ioc_mem_nhdsWithin_Ioi (left_mem_Ico.2 a_lt_c)
[GOAL]
case inr
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[Ici a] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[Ioi a] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[Ioi a] a, y ∈ Ioc a c
⊢ f a ≤ f c
[PROOFSTEP]
rcases(H₁.and H₂).exists with ⟨y, hfy, hy_ac⟩
[GOAL]
case inr.intro.intro
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[Ici a] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[Ioi a] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[Ioi a] a, y ∈ Ioc a c
y : ℝ
hfy : f a ≤ f y
hy_ac : y ∈ Ioc a c
⊢ f a ≤ f c
[PROOFSTEP]
rcases(Convex.mem_Ioc a_lt_c).mp hy_ac with ⟨ya, yc, ya₀, yc₀, yac, rfl⟩
[GOAL]
case inr.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[Ici a] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[Ioi a] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[Ioi a] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
⊢ f a ≤ f c
[PROOFSTEP]
suffices : ya • f a + yc • f a ≤ ya • f a + yc • f c
[GOAL]
case inr.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[Ici a] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[Ioi a] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[Ioi a] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
this : ya • f a + yc • f a ≤ ya • f a + yc • f c
⊢ f a ≤ f c
case this
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[Ici a] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[Ioi a] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[Ioi a] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
⊢ ya • f a + yc • f a ≤ ya • f a + yc • f c
[PROOFSTEP]
exact (smul_le_smul_iff_of_pos yc₀).1 (le_of_add_le_add_left this)
[GOAL]
case this
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[Ici a] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[Ioi a] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[Ioi a] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
⊢ ya • f a + yc • f a ≤ ya • f a + yc • f c
[PROOFSTEP]
calc
  ya • f a + yc • f a = f a := by rw [← add_smul, yac, one_smul]
  _ ≤ f (ya * a + yc * c) := hfy
  _ ≤ ya • f a + yc • f c := h_conv.2 (left_mem_Icc.2 a_lt_b.le) hc ya₀ yc₀.le yac
[GOAL]
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[Ici a] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[Ioi a] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[Ioi a] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
⊢ ya • f a + yc • f a = f a
[PROOFSTEP]
rw [← add_smul, yac, one_smul]
[GOAL]
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
⊢ IsMinOn f s a
[PROOFSTEP]
intro x x_in_s
[GOAL]
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
⊢ x ∈ {x | (fun x => f a ≤ f x) x}
[PROOFSTEP]
let g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
[GOAL]
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
⊢ x ∈ {x | (fun x => f a ≤ f x) x}
[PROOFSTEP]
have hg0 : g 0 = a := AffineMap.lineMap_apply_zero a x
[GOAL]
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : ↑g 0 = a
⊢ x ∈ {x | (fun x => f a ≤ f x) x}
[PROOFSTEP]
have hg1 : g 1 = x := AffineMap.lineMap_apply_one a x
[GOAL]
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : ↑g 0 = a
hg1 : ↑g 1 = x
⊢ x ∈ {x | (fun x => f a ≤ f x) x}
[PROOFSTEP]
have hgc : Continuous g := AffineMap.lineMap_continuous
[GOAL]
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : ↑g 0 = a
hg1 : ↑g 1 = x
hgc : Continuous ↑g
⊢ x ∈ {x | (fun x => f a ≤ f x) x}
[PROOFSTEP]
have h_maps : MapsTo g (Icc 0 1) s := by
  simpa only [mapsTo', ← segment_eq_image_lineMap] using h_conv.1.segment_subset a_in_s x_in_s
[GOAL]
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : ↑g 0 = a
hg1 : ↑g 1 = x
hgc : Continuous ↑g
⊢ MapsTo (↑g) (Icc 0 1) s
[PROOFSTEP]
simpa only [mapsTo', ← segment_eq_image_lineMap] using h_conv.1.segment_subset a_in_s x_in_s
[GOAL]
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : ↑g 0 = a
hg1 : ↑g 1 = x
hgc : Continuous ↑g
h_maps : MapsTo (↑g) (Icc 0 1) s
⊢ x ∈ {x | (fun x => f a ≤ f x) x}
[PROOFSTEP]
have fg_local_min_on : IsLocalMinOn (f ∘ g) (Icc 0 1) 0 :=
  by
  rw [← hg0] at h_localmin
  exact h_localmin.comp_continuousOn h_maps hgc.continuousOn (left_mem_Icc.2 zero_le_one)
[GOAL]
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : ↑g 0 = a
hg1 : ↑g 1 = x
hgc : Continuous ↑g
h_maps : MapsTo (↑g) (Icc 0 1) s
⊢ IsLocalMinOn (f ∘ ↑g) (Icc 0 1) 0
[PROOFSTEP]
rw [← hg0] at h_localmin
[GOAL]
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
h_localmin : IsLocalMinOn f s (↑g 0)
hg0 : ↑g 0 = a
hg1 : ↑g 1 = x
hgc : Continuous ↑g
h_maps : MapsTo (↑g) (Icc 0 1) s
⊢ IsLocalMinOn (f ∘ ↑g) (Icc 0 1) 0
[PROOFSTEP]
exact h_localmin.comp_continuousOn h_maps hgc.continuousOn (left_mem_Icc.2 zero_le_one)
[GOAL]
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : ↑g 0 = a
hg1 : ↑g 1 = x
hgc : Continuous ↑g
h_maps : MapsTo (↑g) (Icc 0 1) s
fg_local_min_on : IsLocalMinOn (f ∘ ↑g) (Icc 0 1) 0
⊢ x ∈ {x | (fun x => f a ≤ f x) x}
[PROOFSTEP]
have fg_min_on : IsMinOn (f ∘ g) (Icc 0 1 : Set ℝ) 0 :=
  by
  refine' IsMinOn.of_isLocalMinOn_of_convexOn_Icc one_pos fg_local_min_on _
  exact (h_conv.comp_affineMap g).subset h_maps (convex_Icc 0 1)
[GOAL]
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : ↑g 0 = a
hg1 : ↑g 1 = x
hgc : Continuous ↑g
h_maps : MapsTo (↑g) (Icc 0 1) s
fg_local_min_on : IsLocalMinOn (f ∘ ↑g) (Icc 0 1) 0
⊢ IsMinOn (f ∘ ↑g) (Icc 0 1) 0
[PROOFSTEP]
refine' IsMinOn.of_isLocalMinOn_of_convexOn_Icc one_pos fg_local_min_on _
[GOAL]
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : ↑g 0 = a
hg1 : ↑g 1 = x
hgc : Continuous ↑g
h_maps : MapsTo (↑g) (Icc 0 1) s
fg_local_min_on : IsLocalMinOn (f ∘ ↑g) (Icc 0 1) 0
⊢ ConvexOn ℝ (Icc 0 1) (f ∘ ↑g)
[PROOFSTEP]
exact (h_conv.comp_affineMap g).subset h_maps (convex_Icc 0 1)
[GOAL]
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : ↑g 0 = a
hg1 : ↑g 1 = x
hgc : Continuous ↑g
h_maps : MapsTo (↑g) (Icc 0 1) s
fg_local_min_on : IsLocalMinOn (f ∘ ↑g) (Icc 0 1) 0
fg_min_on : IsMinOn (f ∘ ↑g) (Icc 0 1) 0
⊢ x ∈ {x | (fun x => f a ≤ f x) x}
[PROOFSTEP]
simpa only [hg0, hg1, comp_apply, mem_setOf_eq] using fg_min_on (right_mem_Icc.2 zero_le_one)


[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
⊢ ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
[PROOFSTEP]
have hε' : 0 < ε / 3 := div_pos hε zero_lt_three
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
⊢ ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
[PROOFSTEP]
obtain ⟨δ, hδ, h⟩ := exists_forall_sphere_dist_add_le_two_sub E hε'
[GOAL]
case intro.intro
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
⊢ ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
[PROOFSTEP]
set δ' := min (1 / 2) (min (ε / 3) <| δ / 3)
[GOAL]
case intro.intro
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
⊢ ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
[PROOFSTEP]
refine' ⟨δ', lt_min one_half_pos <| lt_min hε' (div_pos hδ zero_lt_three), fun x hx y hy hxy => _⟩
[GOAL]
case intro.intro
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
⊢ ‖x + y‖ ≤ 2 - δ'
[PROOFSTEP]
obtain hx' | hx' := le_or_lt ‖x‖ (1 - δ')
[GOAL]
case intro.intro.inl
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : ‖x‖ ≤ 1 - δ'
⊢ ‖x + y‖ ≤ 2 - δ'
[PROOFSTEP]
rw [← one_add_one_eq_two]
[GOAL]
case intro.intro.inl
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : ‖x‖ ≤ 1 - δ'
⊢ ‖x + y‖ ≤ 1 + 1 - δ'
[PROOFSTEP]
exact (norm_add_le_of_le hx' hy).trans (sub_add_eq_add_sub _ _ _).le
[GOAL]
case intro.intro.inr
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
⊢ ‖x + y‖ ≤ 2 - δ'
[PROOFSTEP]
obtain hy' | hy' := le_or_lt ‖y‖ (1 - δ')
[GOAL]
case intro.intro.inr.inl
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : ‖y‖ ≤ 1 - δ'
⊢ ‖x + y‖ ≤ 2 - δ'
[PROOFSTEP]
rw [← one_add_one_eq_two]
[GOAL]
case intro.intro.inr.inl
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : ‖y‖ ≤ 1 - δ'
⊢ ‖x + y‖ ≤ 1 + 1 - δ'
[PROOFSTEP]
exact (norm_add_le_of_le hx hy').trans (add_sub_assoc _ _ _).ge
[GOAL]
case intro.intro.inr.inr
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
⊢ ‖x + y‖ ≤ 2 - δ'
[PROOFSTEP]
have hδ' : 0 < 1 - δ' := sub_pos_of_lt (min_lt_of_left_lt one_half_lt_one)
[GOAL]
case intro.intro.inr.inr
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
⊢ ‖x + y‖ ≤ 2 - δ'
[PROOFSTEP]
have h₁ : ∀ z : E, 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1 := by
  rintro z hz
  rw [norm_smul_of_nonneg (inv_nonneg.2 <| norm_nonneg _), inv_mul_cancel (hδ'.trans hz).ne']
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
⊢ ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
[PROOFSTEP]
rintro z hz
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
z : E
hz : 1 - δ' < ‖z‖
⊢ ‖‖z‖⁻¹ • z‖ = 1
[PROOFSTEP]
rw [norm_smul_of_nonneg (inv_nonneg.2 <| norm_nonneg _), inv_mul_cancel (hδ'.trans hz).ne']
[GOAL]
case intro.intro.inr.inr
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
⊢ ‖x + y‖ ≤ 2 - δ'
[PROOFSTEP]
have h₂ : ∀ z : E, ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ' :=
  by
  rintro z hz hδz
  nth_rw 3 [← one_smul ℝ z]
  rwa [← sub_smul, norm_smul_of_nonneg (sub_nonneg_of_le <| one_le_inv (hδ'.trans_le hδz) hz), sub_mul,
    inv_mul_cancel (hδ'.trans_le hδz).ne', one_mul, sub_le_comm]
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
⊢ ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
[PROOFSTEP]
rintro z hz hδz
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
z : E
hz : ‖z‖ ≤ 1
hδz : 1 - δ' ≤ ‖z‖
⊢ ‖‖z‖⁻¹ • z - z‖ ≤ δ'
[PROOFSTEP]
nth_rw 3 [← one_smul ℝ z]
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
z : E
hz : ‖z‖ ≤ 1
hδz : 1 - δ' ≤ ‖z‖
⊢ ‖‖z‖⁻¹ • z - 1 • z‖ ≤ δ'
[PROOFSTEP]
rwa [← sub_smul, norm_smul_of_nonneg (sub_nonneg_of_le <| one_le_inv (hδ'.trans_le hδz) hz), sub_mul,
  inv_mul_cancel (hδ'.trans_le hδz).ne', one_mul, sub_le_comm]
[GOAL]
case intro.intro.inr.inr
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
⊢ ‖x + y‖ ≤ 2 - δ'
[PROOFSTEP]
set x' := ‖x‖⁻¹ • x
[GOAL]
case intro.intro.inr.inr
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
⊢ ‖x + y‖ ≤ 2 - δ'
[PROOFSTEP]
set y' := ‖y‖⁻¹ • y
[GOAL]
case intro.intro.inr.inr
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
⊢ ‖x + y‖ ≤ 2 - δ'
[PROOFSTEP]
have hxy' : ε / 3 ≤ ‖x' - y'‖ :=
  calc
    ε / 3 = ε - (ε / 3 + ε / 3) := by ring
    _ ≤ ‖x - y‖ - (‖x' - x‖ + ‖y' - y‖) := by
      gcongr
      · exact (h₂ _ hx hx'.le).trans <| min_le_of_right_le <| min_le_left _ _
      · exact (h₂ _ hy hy'.le).trans <| min_le_of_right_le <| min_le_left _ _
    _ ≤ _ := by
      have : ∀ x' y', x - y = x' - y' + (x - x') + (y' - y) := fun _ _ => by abel
      rw [sub_le_iff_le_add, norm_sub_rev _ x, ← add_assoc, this]
      exact norm_add₃_le _ _ _
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
⊢ ε / 3 = ε - (ε / 3 + ε / 3)
[PROOFSTEP]
ring
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
⊢ ε - (ε / 3 + ε / 3) ≤ ‖x - y‖ - (‖x' - x‖ + ‖y' - y‖)
[PROOFSTEP]
gcongr
[GOAL]
case hcd.h₁
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
⊢ ‖x' - x‖ ≤ ε / 3
[PROOFSTEP]
exact (h₂ _ hx hx'.le).trans <| min_le_of_right_le <| min_le_left _ _
[GOAL]
case hcd.h₂
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
⊢ ‖y' - y‖ ≤ ε / 3
[PROOFSTEP]
exact (h₂ _ hy hy'.le).trans <| min_le_of_right_le <| min_le_left _ _
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
⊢ ‖x - y‖ - (‖x' - x‖ + ‖y' - y‖) ≤ ‖x' - y'‖
[PROOFSTEP]
have : ∀ x' y', x - y = x' - y' + (x - x') + (y' - y) := fun _ _ => by abel
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
x✝¹ x✝ : E
⊢ x - y = x✝¹ - x✝ + (x - x✝¹) + (x✝ - y)
[PROOFSTEP]
abel
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
x✝¹ x✝ : E
⊢ x - y = x✝¹ - x✝ + (x - x✝¹) + (x✝ - y)
[PROOFSTEP]
abel
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
this : ∀ (x' y' : E), x - y = x' - y' + (x - x') + (y' - y)
⊢ ‖x - y‖ - (‖x' - x‖ + ‖y' - y‖) ≤ ‖x' - y'‖
[PROOFSTEP]
rw [sub_le_iff_le_add, norm_sub_rev _ x, ← add_assoc, this]
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
this : ∀ (x' y' : E), x - y = x' - y' + (x - x') + (y' - y)
⊢ ‖?x' - ?y' + (x - ?x') + (?y' - y)‖ ≤ ‖x' - y'‖ + ‖x - x'‖ + ‖y' - y‖
case x'
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
this : ∀ (x' y' : E), x - y = x' - y' + (x - x') + (y' - y)
⊢ E
case y'
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
this : ∀ (x' y' : E), x - y = x' - y' + (x - x') + (y' - y)
⊢ E
[PROOFSTEP]
exact norm_add₃_le _ _ _
[GOAL]
case intro.intro.inr.inr
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ ‖x + y‖ ≤ 2 - δ'
[PROOFSTEP]
calc
  ‖x + y‖ ≤ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖ :=
    by
    have : ∀ x' y', x + y = x' + y' + (x - x') + (y - y') := fun _ _ => by abel
    rw [norm_sub_rev, norm_sub_rev y', this]
    exact norm_add₃_le _ _ _
  _ ≤ 2 - δ + δ' + δ' := (add_le_add_three (h (h₁ _ hx') (h₁ _ hy') hxy') (h₂ _ hx hx'.le) (h₂ _ hy hy'.le))
  _ ≤ 2 - δ' := by
    rw [← le_sub_iff_add_le, ← le_sub_iff_add_le, sub_sub, sub_sub]
    refine' sub_le_sub_left _ _
    ring_nf
    rw [← mul_div_cancel' δ three_ne_zero]
    norm_num
      -- Porting note: these three extra lines needed to make `exact` work
    have : 3 * (δ / 3) * (1 / 3) = δ / 3 := by linarith
    rw [this, mul_comm]
    gcongr
    exact min_le_of_right_le <| min_le_right _ _
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ ‖x + y‖ ≤ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖
[PROOFSTEP]
have : ∀ x' y', x + y = x' + y' + (x - x') + (y - y') := fun _ _ => by abel
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
x✝¹ x✝ : E
⊢ x + y = x✝¹ + x✝ + (x - x✝¹) + (y - x✝)
[PROOFSTEP]
abel
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
x✝¹ x✝ : E
⊢ x + y = x✝¹ + x✝ + (x - x✝¹) + (y - x✝)
[PROOFSTEP]
abel
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
this : ∀ (x' y' : E), x + y = x' + y' + (x - x') + (y - y')
⊢ ‖x + y‖ ≤ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖
[PROOFSTEP]
rw [norm_sub_rev, norm_sub_rev y', this]
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
this : ∀ (x' y' : E), x + y = x' + y' + (x - x') + (y - y')
⊢ ‖?x' + ?y' + (x - ?x') + (y - ?y')‖ ≤ ‖x' + y'‖ + ‖x - x'‖ + ‖y - y'‖
case x'
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
this : ∀ (x' y' : E), x + y = x' + y' + (x - x') + (y - y')
⊢ E
case y'
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
this : ∀ (x' y' : E), x + y = x' + y' + (x - x') + (y - y')
⊢ E
[PROOFSTEP]
exact norm_add₃_le _ _ _
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ 2 - δ + δ' + δ' ≤ 2 - δ'
[PROOFSTEP]
rw [← le_sub_iff_add_le, ← le_sub_iff_add_le, sub_sub, sub_sub]
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ 2 - δ ≤ 2 - (δ' + (δ' + δ'))
[PROOFSTEP]
refine' sub_le_sub_left _ _
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ δ' + (δ' + δ') ≤ δ
[PROOFSTEP]
ring_nf
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ min (↑(Int.ofNat 1) / ↑2) (min (ε * (↑(Int.ofNat 1) / ↑3)) (δ * (↑(Int.ofNat 1) / ↑3))) * 3 ≤ δ
[PROOFSTEP]
rw [← mul_div_cancel' δ three_ne_zero]
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ min (↑(Int.ofNat 1) / ↑2) (min (ε * (↑(Int.ofNat 1) / ↑3)) (3 * (δ / 3) * (↑(Int.ofNat 1) / ↑3))) * 3 ≤ 3 * (δ / 3)
[PROOFSTEP]
norm_num
  -- Porting note: these three extra lines needed to make `exact` work
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ min (1 / 2) (min (ε * (1 / 3)) (3 * (δ / 3) * (1 / 3))) * 3 ≤ 3 * (δ / 3)
[PROOFSTEP]
have : 3 * (δ / 3) * (1 / 3) = δ / 3 := by linarith
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ 3 * (δ / 3) * (1 / 3) = δ / 3
[PROOFSTEP]
linarith
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
this : 3 * (δ / 3) * (1 / 3) = δ / 3
⊢ min (1 / 2) (min (ε * (1 / 3)) (3 * (δ / 3) * (1 / 3))) * 3 ≤ 3 * (δ / 3)
[PROOFSTEP]
rw [this, mul_comm]
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
this : 3 * (δ / 3) * (1 / 3) = δ / 3
⊢ 3 * min (1 / 2) (min (ε * (1 / 3)) (δ / 3)) ≤ 3 * (δ / 3)
[PROOFSTEP]
gcongr
[GOAL]
case h
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
this : 3 * (δ / 3) * (1 / 3) = δ / 3
⊢ min (1 / 2) (min (ε * (1 / 3)) (δ / 3)) ≤ δ / 3
[PROOFSTEP]
exact min_le_of_right_le <| min_le_right _ _
[GOAL]
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
⊢ ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
[PROOFSTEP]
obtain hr | hr := le_or_lt r 0
[GOAL]
case inl
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : r ≤ 0
⊢ ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
[PROOFSTEP]
exact
  ⟨1, one_pos, fun x hx y hy h =>
    (hε.not_le <| h.trans <| (norm_sub_le _ _).trans <| add_nonpos (hx.trans hr) (hy.trans hr)).elim⟩
[GOAL]
case inr
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
⊢ ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
[PROOFSTEP]
obtain ⟨δ, hδ, h⟩ := exists_forall_closed_ball_dist_add_le_two_sub E (div_pos hε hr)
[GOAL]
case inr.intro.intro
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
⊢ ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
[PROOFSTEP]
refine' ⟨δ * r, mul_pos hδ hr, fun x hx y hy hxy => _⟩
[GOAL]
case inr.intro.intro
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
x : E
hx : ‖x‖ ≤ r
y : E
hy : ‖y‖ ≤ r
hxy : ε ≤ ‖x - y‖
⊢ ‖x + y‖ ≤ 2 * r - δ * r
[PROOFSTEP]
rw [← div_le_one hr, div_eq_inv_mul, ← norm_smul_of_nonneg (inv_nonneg.2 hr.le)] at hx hy
[GOAL]
case inr.intro.intro
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
x : E
hx✝ : r⁻¹ * ‖x‖ ≤ 1
hx : ‖r⁻¹ • x‖ ≤ 1
y : E
hy✝ : r⁻¹ * ‖y‖ ≤ 1
hy : ‖r⁻¹ • y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
⊢ ‖x + y‖ ≤ 2 * r - δ * r
[PROOFSTEP]
try infer_instance
[GOAL]
case inr.intro.intro
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
x : E
hx✝ : r⁻¹ * ‖x‖ ≤ 1
hx : ‖r⁻¹ • x‖ ≤ 1
y : E
hy✝ : r⁻¹ * ‖y‖ ≤ 1
hy : ‖r⁻¹ • y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
⊢ ‖x + y‖ ≤ 2 * r - δ * r
[PROOFSTEP]
infer_instance
[GOAL]
case inr.intro.intro
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
x : E
hx✝ : r⁻¹ * ‖x‖ ≤ 1
hx : ‖r⁻¹ • x‖ ≤ 1
y : E
hy✝ : r⁻¹ * ‖y‖ ≤ 1
hy : ‖r⁻¹ • y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
⊢ ‖x + y‖ ≤ 2 * r - δ * r
[PROOFSTEP]
have := h hx hy
[GOAL]
case inr.intro.intro
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
x : E
hx✝ : r⁻¹ * ‖x‖ ≤ 1
hx : ‖r⁻¹ • x‖ ≤ 1
y : E
hy✝ : r⁻¹ * ‖y‖ ≤ 1
hy : ‖r⁻¹ • y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
this : ε / r ≤ ‖r⁻¹ • x - r⁻¹ • y‖ → ‖r⁻¹ • x + r⁻¹ • y‖ ≤ 2 - δ
⊢ ‖x + y‖ ≤ 2 * r - δ * r
[PROOFSTEP]
simp_rw [← smul_add, ← smul_sub, norm_smul_of_nonneg (inv_nonneg.2 hr.le), ← div_eq_inv_mul, div_le_div_right hr,
  div_le_iff hr, sub_mul] at this
[GOAL]
case inr.intro.intro
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
x : E
hx✝ : r⁻¹ * ‖x‖ ≤ 1
hx : ‖r⁻¹ • x‖ ≤ 1
y : E
hy✝ : r⁻¹ * ‖y‖ ≤ 1
hy : ‖r⁻¹ • y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
this : ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ * r
⊢ ‖x + y‖ ≤ 2 * r - δ * r
[PROOFSTEP]
exact this hxy


[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
have hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p := by simpa using h.left_ne_right
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ p₁ -ᵥ p ≠ p₃ -ᵥ p
[PROOFSTEP]
simpa using h.left_ne_right
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
rw [Sbtw, ← wbtw_vsub_const_iff p, Wbtw, affineSegment_eq_segment, ← insert_endpoints_openSegment, Set.mem_insert_iff,
  Set.mem_insert_iff] at h
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : (p₂ -ᵥ p = p₁ -ᵥ p ∨ p₂ -ᵥ p = p₃ -ᵥ p ∨ p₂ -ᵥ p ∈ openSegment ℝ (p₁ -ᵥ p) (p₃ -ᵥ p)) ∧ p₂ ≠ p₁ ∧ p₂ ≠ p₃
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
rcases h with ⟨h | h | h, hp₂p₁, hp₂p₃⟩
[GOAL]
case intro.inl.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ -ᵥ p = p₁ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
rw [vsub_left_cancel_iff] at h
[GOAL]
case intro.inl.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ = p₁
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
exact False.elim (hp₂p₁ h)
[GOAL]
case intro.inr.inl.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ -ᵥ p = p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
rw [vsub_left_cancel_iff] at h
[GOAL]
case intro.inr.inl.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ = p₃
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
exact False.elim (hp₂p₃ h)
[GOAL]
case intro.inr.inr.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ -ᵥ p ∈ openSegment ℝ (p₁ -ᵥ p) (p₃ -ᵥ p)
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
rw [openSegment_eq_image, Set.mem_image] at h
[GOAL]
case intro.inr.inr.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : ∃ x, x ∈ Set.Ioo 0 1 ∧ (1 - x) • (p₁ -ᵥ p) + x • (p₃ -ᵥ p) = p₂ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
rcases h with ⟨r, ⟨hr0, hr1⟩, hr⟩
[GOAL]
case intro.inr.inr.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
r : ℝ
hr : (1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p) = p₂ -ᵥ p
hr0 : 0 < r
hr1 : r < 1
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
simp_rw [@dist_eq_norm_vsub V, ← hr]
[GOAL]
case intro.inr.inr.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
r : ℝ
hr : (1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p) = p₂ -ᵥ p
hr0 : 0 < r
hr1 : r < 1
⊢ ‖(1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p)‖ < max ‖p₁ -ᵥ p‖ ‖p₃ -ᵥ p‖
[PROOFSTEP]
exact norm_combo_lt_of_ne (le_max_left _ _) (le_max_right _ _) hp₁p₃ (sub_pos.2 hr1) hr0 (by abel)
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
r : ℝ
hr : (1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p) = p₂ -ᵥ p
hr0 : 0 < r
hr1 : r < 1
⊢ 1 - r + r = 1
[PROOFSTEP]
abel
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
r : ℝ
hr : (1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p) = p₂ -ᵥ p
hr0 : 0 < r
hr1 : r < 1
⊢ 1 - r + r = 1
[PROOFSTEP]
abel
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
by_cases hp₁ : p₂ = p₁
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₁ : p₂ = p₁
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
simp [hp₁]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₁ : ¬p₂ = p₁
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
by_cases hp₃ : p₂ = p₃
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₁ : ¬p₂ = p₁
hp₃ : p₂ = p₃
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
simp [hp₃]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₁ : ¬p₂ = p₁
hp₃ : ¬p₂ = p₃
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
have hs : Sbtw ℝ p₁ p₂ p₃ := ⟨h, hp₁, hp₃⟩
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₁ : ¬p₂ = p₁
hp₃ : ¬p₂ = p₃
hs : Sbtw ℝ p₁ p₂ p₃
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
[PROOFSTEP]
exact (hs.dist_lt_max_dist _).le
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
rcases h.wbtw_or_wbtw_or_wbtw with (hw | hw | hw)
[GOAL]
case inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₁ p₂ p₃
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
exact hw
[GOAL]
case inr.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
by_cases hp₃p₂ : p₃ = p₂
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
hp₃p₂ : p₃ = p₂
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
simp [hp₃p₂]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
hp₃p₂ : ¬p₃ = p₂
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
have hs : Sbtw ℝ p₂ p₃ p₁ := ⟨hw, hp₃p₂, hp₁p₃.symm⟩
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
hp₃p₂ : ¬p₃ = p₂
hs : Sbtw ℝ p₂ p₃ p₁
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
have hs' := hs.dist_lt_max_dist p
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
hp₃p₂ : ¬p₃ = p₂
hs : Sbtw ℝ p₂ p₃ p₁
hs' : dist p₃ p < max (dist p₂ p) (dist p₁ p)
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
rw [hp₁, hp₃, lt_max_iff, lt_self_iff_false, or_false_iff] at hs'
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
hp₃p₂ : ¬p₃ = p₂
hs : Sbtw ℝ p₂ p₃ p₁
hs' : r < dist p₂ p
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
exact False.elim (hp₂.not_lt hs')
[GOAL]
case inr.inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
by_cases hp₁p₂ : p₁ = p₂
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : p₁ = p₂
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
simp [hp₁p₂]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : ¬p₁ = p₂
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
have hs : Sbtw ℝ p₃ p₁ p₂ := ⟨hw, hp₁p₃, hp₁p₂⟩
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : ¬p₁ = p₂
hs : Sbtw ℝ p₃ p₁ p₂
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
have hs' := hs.dist_lt_max_dist p
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : ¬p₁ = p₂
hs : Sbtw ℝ p₃ p₁ p₂
hs' : dist p₁ p < max (dist p₃ p) (dist p₂ p)
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
rw [hp₁, hp₃, lt_max_iff, lt_self_iff_false, false_or_iff] at hs'
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : ¬p₁ = p₂
hs : Sbtw ℝ p₃ p₁ p₂
hs' : r < dist p₂ p
⊢ Wbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
exact False.elim (hp₂.not_lt hs')
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p < r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
⊢ Sbtw ℝ p₁ p₂ p₃
[PROOFSTEP]
refine' ⟨h.wbtw_of_dist_eq_of_dist_le hp₁ hp₂.le hp₃ hp₁p₃, _, _⟩
[GOAL]
case refine'_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p < r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
⊢ p₂ ≠ p₁
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₂ p₃ : P
r : ℝ
hp₂ : dist p₂ p < r
hp₃ : dist p₃ p = r
h : Collinear ℝ {p₂, p₂, p₃}
hp₁ : dist p₂ p = r
hp₁p₃ : p₂ ≠ p₃
⊢ False
[PROOFSTEP]
exact hp₂.ne hp₁
[GOAL]
case refine'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p < r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
⊢ p₂ ≠ p₃
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : StrictConvexSpace ℝ V
p p₁ p₂ : P
r : ℝ
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p < r
h : Collinear ℝ {p₁, p₂, p₂}
hp₃ : dist p₂ p = r
hp₁p₃ : p₁ ≠ p₂
⊢ False
[PROOFSTEP]
exact hp₂.ne hp₃


[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝ : Fintype ι
⊢ stdSimplex ℝ ι ⊆ closedBall 0 1
[PROOFSTEP]
intro f hf
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
⊢ f ∈ closedBall 0 1
[PROOFSTEP]
rw [Metric.mem_closedBall, dist_pi_le_iff zero_le_one]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
⊢ ∀ (b : ι), dist (f b) (OfNat.ofNat 0 b) ≤ 1
[PROOFSTEP]
intro x
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
x : ι
⊢ dist (f x) (OfNat.ofNat 0 x) ≤ 1
[PROOFSTEP]
rw [Pi.zero_apply, Real.dist_0_eq_abs, abs_of_nonneg <| hf.1 x]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
x : ι
⊢ f x ≤ 1
[PROOFSTEP]
exact (mem_Icc_of_mem_stdSimplex hf x).2
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁸ : LinearOrderedRing 𝕜
inst✝⁷ : DenselyOrdered 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : OrderTopology 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ [x-[𝕜]y] ⊆ closure (openSegment 𝕜 x y)
[PROOFSTEP]
rw [segment_eq_image, openSegment_eq_image, ← closure_Ioo (zero_ne_one' 𝕜)]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁸ : LinearOrderedRing 𝕜
inst✝⁷ : DenselyOrdered 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : OrderTopology 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ (fun θ => (1 - θ) • x + θ • y) '' closure (Ioo 0 1) ⊆ closure ((fun θ => (1 - θ) • x + θ • y) '' Ioo 0 1)
[PROOFSTEP]
exact image_closure_subset_closure_image (by continuity)
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁸ : LinearOrderedRing 𝕜
inst✝⁷ : DenselyOrdered 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : OrderTopology 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ Continuous fun θ => (1 - θ) • x + θ • y
[PROOFSTEP]
continuity
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝¹¹ : LinearOrderedRing 𝕜
inst✝¹⁰ : DenselyOrdered 𝕜
inst✝⁹ : PseudoMetricSpace 𝕜
inst✝⁸ : OrderTopology 𝕜
inst✝⁷ : ProperSpace 𝕜
inst✝⁶ : CompactIccSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ closure (openSegment 𝕜 x y) = [x-[𝕜]y]
[PROOFSTEP]
rw [segment_eq_image, openSegment_eq_image, ← closure_Ioo (zero_ne_one' 𝕜)]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝¹¹ : LinearOrderedRing 𝕜
inst✝¹⁰ : DenselyOrdered 𝕜
inst✝⁹ : PseudoMetricSpace 𝕜
inst✝⁸ : OrderTopology 𝕜
inst✝⁷ : ProperSpace 𝕜
inst✝⁶ : CompactIccSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ closure ((fun θ => (1 - θ) • x + θ • y) '' Ioo 0 1) = (fun θ => (1 - θ) • x + θ • y) '' closure (Ioo 0 1)
[PROOFSTEP]
exact (image_closure_of_isCompact (bounded_Ioo _ _).isCompact_closure <| Continuous.continuousOn <| by continuity).symm
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝¹¹ : LinearOrderedRing 𝕜
inst✝¹⁰ : DenselyOrdered 𝕜
inst✝⁹ : PseudoMetricSpace 𝕜
inst✝⁸ : OrderTopology 𝕜
inst✝⁷ : ProperSpace 𝕜
inst✝⁶ : CompactIccSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ Continuous fun θ => (1 - θ) • x + θ • y
[PROOFSTEP]
continuity
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 < a
hb : 0 ≤ b
hab : a + b = 1
⊢ interior (a • s) + closure (b • s) = interior (a • s) + b • s
[PROOFSTEP]
rw [isOpen_interior.add_closure (b • s)]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ a • closure s + b • interior s ⊆ interior s
[PROOFSTEP]
rw [add_comm]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ b • interior s + a • closure s ⊆ interior s
[PROOFSTEP]
exact hs.combo_interior_closure_subset_interior hb ha (add_comm a b ▸ hab)
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ a • s + b • interior s ⊆ interior s
[PROOFSTEP]
rw [add_comm]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ b • interior s + a • s ⊆ interior s
[PROOFSTEP]
exact hs.combo_interior_self_subset_interior hb ha (add_comm a b ▸ hab)
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ interior s
hy : y ∈ closure s
⊢ openSegment 𝕜 x y ⊆ interior s
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, hab, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ interior s
hy : y ∈ closure s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s
[PROOFSTEP]
exact hs.combo_interior_closure_mem_interior hx hy ha hb.le hab
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ closure s
hy : y ∈ interior s
⊢ openSegment 𝕜 x y ⊆ interior s
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, hab, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ closure s
hy : y ∈ interior s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s
[PROOFSTEP]
exact hs.combo_closure_interior_mem_interior hx hy ha.le hb hab
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ closure s
hy : y ∈ interior s
t : 𝕜
ht : t ∈ Ioc 0 1
⊢ x + t • (y - x) ∈ interior s
[PROOFSTEP]
simpa only [sub_smul, smul_sub, one_smul, add_sub, add_comm] using
  hs.combo_interior_closure_mem_interior hy hx ht.1 (sub_nonneg.mpr ht.2) (add_sub_cancel'_right _ _)
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ closure s
hy : x + y ∈ interior s
t : 𝕜
ht : t ∈ Ioc 0 1
⊢ x + t • y ∈ interior s
[PROOFSTEP]
simpa only [add_sub_cancel'] using hs.add_smul_sub_mem_interior' hx hy ht
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => ∃ c, ↑(lineMap x y) c ∈ interior s
⊢ StrictConvex 𝕜 s
[PROOFSTEP]
refine' strictConvex_iff_openSegment_subset.2 _
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => ∃ c, ↑(lineMap x y) c ∈ interior s
⊢ Set.Pairwise s fun x y => openSegment 𝕜 x y ⊆ interior s
[PROOFSTEP]
intro x hx y hy hne
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => ∃ c, ↑(lineMap x y) c ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
⊢ openSegment 𝕜 x y ⊆ interior s
[PROOFSTEP]
by_cases hx' : x ∈ interior s
[GOAL]
case pos
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => ∃ c, ↑(lineMap x y) c ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
hx' : x ∈ interior s
⊢ openSegment 𝕜 x y ⊆ interior s
[PROOFSTEP]
exact hs.openSegment_interior_self_subset_interior hx' hy
[GOAL]
case neg
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => ∃ c, ↑(lineMap x y) c ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
hx' : ¬x ∈ interior s
⊢ openSegment 𝕜 x y ⊆ interior s
[PROOFSTEP]
by_cases hy' : y ∈ interior s
[GOAL]
case pos
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => ∃ c, ↑(lineMap x y) c ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
hx' : ¬x ∈ interior s
hy' : y ∈ interior s
⊢ openSegment 𝕜 x y ⊆ interior s
[PROOFSTEP]
exact hs.openSegment_self_interior_subset_interior hx hy'
[GOAL]
case neg
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => ∃ c, ↑(lineMap x y) c ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
hx' : ¬x ∈ interior s
hy' : ¬y ∈ interior s
⊢ openSegment 𝕜 x y ⊆ interior s
[PROOFSTEP]
rcases h ⟨hx, hx'⟩ ⟨hy, hy'⟩ hne with ⟨c, hc⟩
[GOAL]
case neg.intro
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => ∃ c, ↑(lineMap x y) c ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
hx' : ¬x ∈ interior s
hy' : ¬y ∈ interior s
c : 𝕜
hc : ↑(lineMap x y) c ∈ interior s
⊢ openSegment 𝕜 x y ⊆ interior s
[PROOFSTEP]
refine' (openSegment_subset_union x y ⟨c, rfl⟩).trans (insert_subset_iff.2 ⟨hc, union_subset _ _⟩)
[GOAL]
case neg.intro.refine'_1
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => ∃ c, ↑(lineMap x y) c ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
hx' : ¬x ∈ interior s
hy' : ¬y ∈ interior s
c : 𝕜
hc : ↑(lineMap x y) c ∈ interior s
⊢ openSegment 𝕜 x (↑(lineMap x y) c) ⊆ interior s
case neg.intro.refine'_2
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => ∃ c, ↑(lineMap x y) c ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
hx' : ¬x ∈ interior s
hy' : ¬y ∈ interior s
c : 𝕜
hc : ↑(lineMap x y) c ∈ interior s
⊢ openSegment 𝕜 (↑(lineMap x y) c) y ⊆ interior s
[PROOFSTEP]
exacts [hs.openSegment_self_interior_subset_interior hx hc, hs.openSegment_interior_self_subset_interior hc hy]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => Set.Nonempty ([x-[𝕜]y] \ frontier s)
⊢ StrictConvex 𝕜 s
[PROOFSTEP]
refine' hs.strictConvex' <| h.imp_on fun x hx y hy _ => _
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => Set.Nonempty ([x-[𝕜]y] \ frontier s)
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
⊢ fun ⦃a b⦄ => Set.Nonempty ([a-[𝕜]b] \ frontier s) → ∃ c, ↑(lineMap a b) c ∈ interior s
[PROOFSTEP]
simp only [segment_eq_image_lineMap, ← self_diff_frontier]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => Set.Nonempty ([x-[𝕜]y] \ frontier s)
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
⊢ Set.Nonempty ((fun a => ↑(lineMap x y) a) '' Icc 0 1 \ frontier s) → ∃ c, ↑(lineMap x y) c ∈ s \ frontier s
[PROOFSTEP]
rintro ⟨_, ⟨⟨c, hc, rfl⟩, hcs⟩⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => Set.Nonempty ([x-[𝕜]y] \ frontier s)
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
c : 𝕜
hc : c ∈ Icc 0 1
hcs : ¬(fun a => ↑(lineMap x y) a) c ∈ frontier s
⊢ ∃ c, ↑(lineMap x y) c ∈ s \ frontier s
[PROOFSTEP]
refine' ⟨c, hs.segment_subset hx.1 hy.1 _, hcs⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : Set.Pairwise (s \ interior s) fun x y => Set.Nonempty ([x-[𝕜]y] \ frontier s)
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
c : 𝕜
hc : c ∈ Icc 0 1
hcs : ¬(fun a => ↑(lineMap x y) a) c ∈ frontier s
⊢ ↑(lineMap x y) c ∈ [x-[𝕜]y]
[PROOFSTEP]
exact (segment_eq_image_lineMap 𝕜 x y).symm ▸ mem_image_of_mem _ hc
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Set.Finite s
⊢ IsCompact (↑(convexHull ℝ) s)
[PROOFSTEP]
rw [hs.convexHull_eq_image]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Set.Finite s
⊢ IsCompact (↑(Finset.sum Finset.univ fun x => LinearMap.smulRight (LinearMap.proj x) ↑x) '' stdSimplex ℝ ↑s)
[PROOFSTEP]
apply (@isCompact_stdSimplex _ hs.fintype).image
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Set.Finite s
⊢ Continuous ↑(Finset.sum Finset.univ fun x => LinearMap.smulRight (LinearMap.proj x) ↑x)
[PROOFSTEP]
haveI := hs.fintype
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Set.Finite s
this : Fintype ↑s
⊢ Continuous ↑(Finset.sum Finset.univ fun x => LinearMap.smulRight (LinearMap.proj x) ↑x)
[PROOFSTEP]
apply LinearMap.continuous_on_pi
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
⊢ closure s ⊆ ↑(homothety x t) '' interior s
[PROOFSTEP]
intro y hy
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
⊢ y ∈ ↑(homothety x t) '' interior s
[PROOFSTEP]
have hne : t ≠ 0 := (one_pos.trans ht).ne'
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
hne : t ≠ 0
⊢ y ∈ ↑(homothety x t) '' interior s
[PROOFSTEP]
refine'
  ⟨homothety x t⁻¹ y, hs.openSegment_interior_closure_subset_interior hx hy _,
    (AffineEquiv.homothetyUnitsMulHom x (Units.mk0 t hne)).apply_symm_apply y⟩
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
hne : t ≠ 0
⊢ ↑(homothety x t⁻¹) y ∈ openSegment ℝ x y
[PROOFSTEP]
rw [openSegment_eq_image_lineMap, ← inv_one, ← inv_Ioi (zero_lt_one' ℝ), ← image_inv, image_image, homothety_eq_lineMap]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
hne : t ≠ 0
⊢ ↑(lineMap x y) t⁻¹ ∈ (fun x_1 => ↑(lineMap x y) x_1⁻¹) '' Ioi 1
[PROOFSTEP]
exact mem_image_of_mem _ ht
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : Set.Nonempty s
⊢ IsPathConnected s
[PROOFSTEP]
refine' isPathConnected_iff.mpr ⟨hne, _⟩
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : Set.Nonempty s
⊢ ∀ (x : E), x ∈ s → ∀ (y : E), y ∈ s → JoinedIn s x y
[PROOFSTEP]
intro x x_in y y_in
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : Set.Nonempty s
x : E
x_in : x ∈ s
y : E
y_in : y ∈ s
⊢ JoinedIn s x y
[PROOFSTEP]
have H := hconv.segment_subset x_in y_in
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : Set.Nonempty s
x : E
x_in : x ∈ s
y : E
y_in : y ∈ s
H : [x-[ℝ]y] ⊆ s
⊢ JoinedIn s x y
[PROOFSTEP]
rw [segment_eq_image_lineMap] at H
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : Set.Nonempty s
x : E
x_in : x ∈ s
y : E
y_in : y ∈ s
H : ↑(lineMap x y) '' Icc 0 1 ⊆ s
⊢ JoinedIn s x y
[PROOFSTEP]
exact JoinedIn.ofLine AffineMap.lineMap_continuous.continuousOn (lineMap_apply_zero _ _) (lineMap_apply_one _ _) H