Theorem: Convex.inter_ball
Proof state before:
case mk.mk.intro.mk.intro.intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ s
Tactic:
apply c m0 m1
Proof state after:
case mk.mk.intro.mk.intro.intro.a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ 0 ≤ r1 / (r0 + r1)

case mk.mk.intro.mk.intro.intro.a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ 0 ≤ r0 / (r0 + r1)

case mk.mk.intro.mk.intro.intro.a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f✝ : E → α
z : E
c : Convex ℝ s
r0 r1 : ℝ
r0p : 0 < r0
r1p : 0 < r1
x0 : E
m0✝ : x0 ∈ closure s
x1 : E
m1✝ : x1 ∈ closure s
ne : ∃ z, z ∈ ball (↑⟨x0, m0✝⟩) r0 ∩ ball (↑⟨x1, m1✝⟩) r1
x01 : ‖x1 - x0‖ < r0 + r1
sub : ∀ (x : E) {a b : ℝ}, 0 < a → 0 < b → (a / (a + b)) • x - x = -((b / (a + b)) • x)
le : ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
e : ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
f : ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
z0 z1 : E
m : (r1 / (r0 + r1)) • (z0, z1).1 + (r0 / (r0 + r1)) • (z0, z1).2 ∈ ball x0 r0 ∩ ball x1 r1
m0 : (z0, z1).1 ∈ s
m1 : (z0, z1).2 ∈ s
⊢ r1 / (r0 + r1) + r0 / (r0 + r1) = 1