internlm/Lean-Github huggingface dataset:
Theorem: Convex.inter_ball
Proof state before:
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)
⊢ ∀ {a : ℝ}, 0 < a → a / (r0 + r1) * ‖x1 - x0‖ < a
Tactic:
intro a ap
Proof state after:
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)
a : ℝ
ap : 0 < a
⊢ a / (r0 + r1) * ‖x1 - x0‖ < a
Theorem: Convex.inter_ball
Proof state before:
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)
a : ℝ
ap : 0 < a
⊢ a / (r0 + r1) * ‖x1 - x0‖ < a
Tactic:
apply lt_of_lt_of_le (mul_lt_mul_of_pos_left x01 (div_pos ap (add_pos r0p r1p)))
Proof state after:
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)
a : ℝ
ap : 0 < a
⊢ a / (r0 + r1) * (r0 + r1) ≤ a
Theorem: Convex.inter_ball
Proof state before:
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)
a : ℝ
ap : 0 < a
⊢ a / (r0 + r1) * (r0 + r1) ≤ a
Tactic:
rw [div_mul_cancel₀ _ (add_pos r0p r1p).ne']
Proof state after:
no goals
Theorem: Convex.inter_ball
Proof state before:
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
⊢ ∀ᶠ (p : E × E) in 𝓝 (x0, x1), (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2 ∈ ball x0 r0 ∩ ball x1 r1
Tactic:
refine ContinuousAt.eventually_mem ?_ ((isOpen_ball.inter isOpen_ball).mem_nhds ?_)
Proof state after:
case refine_1
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
⊢ ContinuousAt (fun p => (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2) (x0, x1)

case refine_2
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
⊢ (r1 / (r0 + r1)) • (x0, x1).1 + (r0 / (r0 + r1)) • (x0, x1).2 ∈ ball x0 r0 ∩ ball x1 r1
Theorem: Convex.inter_ball
Proof state before:
case refine_1
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
⊢ ContinuousAt (fun p => (r1 / (r0 + r1)) • p.1 + (r0 / (r0 + r1)) • p.2) (x0, x1)
Tactic:
exact ((continuous_fst.const_smul _).add (continuous_snd.const_smul _)).continuousAt
Proof state after:
no goals
Theorem: Convex.inter_ball
Proof state before:
case refine_2
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
⊢ (r1 / (r0 + r1)) • (x0, x1).1 + (r0 / (r0 + r1)) • (x0, x1).2 ∈ ball x0 r0 ∩ ball x1 r1
Tactic:
simp only [mem_inter_iff, mem_ball, dist_eq_norm, ← sub_add_eq_add_sub _ x0 _,
  add_sub_assoc _ _ x1]
Proof state after:
case refine_2
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
⊢ ‖(r1 / (r0 + r1)) • x0 - x0 + (r0 / (r0 + r1)) • x1‖ < r0 ∧
    ‖(r1 / (r0 + r1)) • x0 + ((r0 / (r0 + r1)) • x1 - x1)‖ < r1
Theorem: Convex.inter_ball
Proof state before:
case refine_2
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
⊢ ‖(r1 / (r0 + r1)) • x0 - x0 + (r0 / (r0 + r1)) • x1‖ < r0 ∧
    ‖(r1 / (r0 + r1)) • x0 + ((r0 / (r0 + r1)) • x1 - x1)‖ < r1
Tactic:
nth_rw 1 [add_comm r0 r1]
Proof state after:
case refine_2
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
⊢ ‖(r1 / (r1 + r0)) • x0 - x0 + (r0 / (r0 + r1)) • x1‖ < r0 ∧
    ‖(r1 / (r0 + r1)) • x0 + ((r0 / (r0 + r1)) • x1 - x1)‖ < r1
Theorem: Convex.inter_ball
Proof state before:
case refine_2
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
⊢ ‖(r1 / (r1 + r0)) • x0 - x0 + (r0 / (r0 + r1)) • x1‖ < r0 ∧
    ‖(r1 / (r0 + r1)) • x0 + ((r0 / (r0 + r1)) • x1 - x1)‖ < r1
Tactic:
simp only [sub _ r0p r1p, sub _ r1p r0p]
Proof state after:
case refine_2
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
⊢ ‖-((r0 / (r1 + r0)) • x0) + (r0 / (r0 + r1)) • x1‖ < r0 ∧ ‖(r1 / (r0 + r1)) • x0 + -((r1 / (r0 + r1)) • x1)‖ < r1
Theorem: Convex.inter_ball
Proof state before:
case refine_2
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
⊢ ‖-((r0 / (r1 + r0)) • x0) + (r0 / (r0 + r1)) • x1‖ < r0 ∧ ‖(r1 / (r0 + r1)) • x0 + -((r1 / (r0 + r1)) • x1)‖ < r1
Tactic:
simp only [add_comm r1 r0, neg_add_eq_sub, ← sub_eq_add_neg, ← smul_sub, norm_smul,
  Real.norm_eq_abs, abs_div, abs_of_pos r0p, abs_of_pos r1p, abs_of_pos (add_pos r0p r1p),
  norm_sub_rev (x0 : E) x1]
Proof state after:
case refine_2
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
⊢ r0 / (r0 + r1) * ‖x1 - x0‖ < r0 ∧ r1 / (r0 + r1) * ‖x1 - x0‖ < r1
Theorem: Convex.inter_ball
Proof state before:
case refine_2
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
⊢ r0 / (r0 + r1) * ‖x1 - x0‖ < r0 ∧ r1 / (r0 + r1) * ‖x1 - x0‖ < r1
Tactic:
use le r0p, le r1p
Proof state after:
no goals
Theorem: Convex.inter_ball
Proof state before:
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
⊢ ∃ᶠ (p : E × E) in 𝓝 (x0, x1), p.1 ∈ s ∧ p.2 ∈ s
Tactic:
simp only [nhds_prod_eq]
Proof state after:
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
⊢ ∃ᶠ (p : E × E) in 𝓝 x0 ×ˢ 𝓝 x1, p.1 ∈ s ∧ p.2 ∈ s
Theorem: Convex.inter_ball
Proof state before:
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
⊢ ∃ᶠ (p : E × E) in 𝓝 x0 ×ˢ 𝓝 x1, p.1 ∈ s ∧ p.2 ∈ s
Tactic:
rw [Prod.frequently (p := fun x ↦ x ∈ s) (q := fun x ↦ x ∈ s)]
Proof state after:
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
⊢ (∃ᶠ (a : E) in 𝓝 x0, a ∈ s) ∧ ∃ᶠ (b : E) in 𝓝 x1, b ∈ s
Theorem: Convex.inter_ball
Proof state before:
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
⊢ (∃ᶠ (a : E) in 𝓝 x0, a ∈ s) ∧ ∃ᶠ (b : E) in 𝓝 x1, b ∈ s
Tactic:
use mem_closure_iff_frequently.mp m0, mem_closure_iff_frequently.mp m1
Proof state after:
no goals
Theorem: Base.ug
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : ↑(closure s)
⊢ EqOn b.u (b.g x) (b.t ∩ Metric.ball (↑x) (b.r x))
Tactic:
intro z ⟨zt, m⟩
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
x : ↑(closure s)
z : E
zt : z ∈ b.t
m : z ∈ Metric.ball (↑x) (b.r x)
⊢ b.u z = b.g x z
Theorem: Base.ug
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
x : ↑(closure s)
z : E
zt : z ∈ b.t
m : z ∈ Metric.ball (↑x) (b.r x)
⊢ b.u z = b.g x z
Tactic:
simp only [Base.u, zt, dif_pos]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
x : ↑(closure s)
z : E
zt : z ∈ b.t
m : z ∈ Metric.ball (↑x) (b.r x)
⊢ b.g (b.y ⋯) z = b.g x z
Theorem: Base.ug
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
x : ↑(closure s)
z : E
zt : z ∈ b.t
m : z ∈ Metric.ball (↑x) (b.r x)
⊢ b.g (b.y ⋯) z = b.g x z
Tactic:
refine b.unique (isOpen_ball.inter isOpen_ball)
  ((convex_ball _ _).inter (convex_ball _ _)).isPreconnected
  (fun _ m ↦ b.gp _ (inter_subset_left _ _ m)) (fun _ m ↦ b.gp _ (inter_subset_right _ _ m))
  ?_ ⟨b.yt zt, m⟩
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
x : ↑(closure s)
z : E
zt : z ∈ b.t
m : z ∈ Metric.ball (↑x) (b.r x)
⊢ ∃ x_1 ∈ Metric.ball (↑(b.y ⋯)) (b.r (b.y ⋯)) ∩ Metric.ball (↑x) (b.r x), b.g (b.y ⋯) x_1 = b.g x x_1
Theorem: Base.ug
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
x : ↑(closure s)
z : E
zt : z ∈ b.t
m : z ∈ Metric.ball (↑x) (b.r x)
⊢ ∃ x_1 ∈ Metric.ball (↑(b.y ⋯)) (b.r (b.y ⋯)) ∩ Metric.ball (↑x) (b.r x), b.g (b.y ⋯) x_1 = b.g x x_1
Tactic:
rcases b.convex.inter_ball (b.y zt) x (b.rp _) (b.rp _) ⟨_, ⟨b.yt zt, m⟩⟩ with ⟨w, m⟩
Proof state after:
case intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
x : ↑(closure s)
z : E
zt : z ∈ b.t
m✝ : z ∈ Metric.ball (↑x) (b.r x)
w : E
m : w ∈ s ∩ Metric.ball (↑(b.y zt)) (b.r (b.y zt)) ∩ Metric.ball (↑x) (b.r x)
⊢ ∃ x_1 ∈ Metric.ball (↑(b.y ⋯)) (b.r (b.y ⋯)) ∩ Metric.ball (↑x) (b.r x), b.g (b.y ⋯) x_1 = b.g x x_1
Theorem: Base.ug
Proof state before:
case intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
x : ↑(closure s)
z : E
zt : z ∈ b.t
m✝ : z ∈ Metric.ball (↑x) (b.r x)
w : E
m : w ∈ s ∩ Metric.ball (↑(b.y zt)) (b.r (b.y zt)) ∩ Metric.ball (↑x) (b.r x)
⊢ ∃ x_1 ∈ Metric.ball (↑(b.y ⋯)) (b.r (b.y ⋯)) ∩ Metric.ball (↑x) (b.r x), b.g (b.y ⋯) x_1 = b.g x x_1
Tactic:
exact ⟨w, ⟨m.1.2, m.2⟩, _root_.trans ((b.gf _).self_of_nhdsSet ⟨m.1.1, m.1.2⟩)
  ((b.gf x).self_of_nhdsSet ⟨m.1.1, m.2⟩).symm⟩
Proof state after:
no goals
Theorem: Base.uf
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
⊢ (𝓝ˢ s).EventuallyEq b.u f
Tactic:
simp only [Filter.EventuallyEq, Filter.eventually_iff, mem_nhdsSet_iff_forall]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
⊢ ∀ x ∈ s, {x | b.u x = f x} ∈ 𝓝 x
Theorem: Base.uf
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
⊢ ∀ x ∈ s, {x | b.u x = f x} ∈ 𝓝 x
Tactic:
intro z m
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
z : E
m : z ∈ s
⊢ {x | b.u x = f x} ∈ 𝓝 z
Theorem: Base.uf
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
z : E
m : z ∈ s
⊢ {x | b.u x = f x} ∈ 𝓝 z
Tactic:
simp only [← Filter.eventually_iff]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
z : E
m : z ∈ s
⊢ ∀ᶠ (x : E) in 𝓝 z, b.u x = f x
Theorem: Base.uf
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
z : E
m : z ∈ s
⊢ ∀ᶠ (x : E) in 𝓝 z, b.u x = f x
Tactic:
set x : closure s := ⟨z, subset_closure m⟩
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
z : E
m : z ∈ s
x : ↑(closure s) := ⟨z, ⋯⟩
⊢ ∀ᶠ (x : E) in 𝓝 z, b.u x = f x
Theorem: Base.uf
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
z : E
m : z ∈ s
x : ↑(closure s) := ⟨z, ⋯⟩
⊢ ∀ᶠ (x : E) in 𝓝 z, b.u x = f x
Tactic:
have zs : z ∈ Metric.ball (x : E) (b.r x) := mem_ball_self (b.rp x)
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
z : E
m : z ∈ s
x : ↑(closure s) := ⟨z, ⋯⟩
zs : z ∈ Metric.ball (↑x) (b.r x)
⊢ ∀ᶠ (x : E) in 𝓝 z, b.u x = f x
Theorem: Base.uf
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
z : E
m : z ∈ s
x : ↑(closure s) := ⟨z, ⋯⟩
zs : z ∈ Metric.ball (↑x) (b.r x)
⊢ ∀ᶠ (x : E) in 𝓝 z, b.u x = f x
Tactic:
have ug := (b.ug x).eventuallyEq_of_mem ((b.ot.inter isOpen_ball).mem_nhds
  ⟨b.cover (subset_closure m), zs⟩)
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
z : E
m : z ∈ s
x : ↑(closure s) := ⟨z, ⋯⟩
zs : z ∈ Metric.ball (↑x) (b.r x)
ug : (𝓝 z).EventuallyEq b.u (b.g x)
⊢ ∀ᶠ (x : E) in 𝓝 z, b.u x = f x
Theorem: Base.uf
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
z : E
m : z ∈ s
x : ↑(closure s) := ⟨z, ⋯⟩
zs : z ∈ Metric.ball (↑x) (b.r x)
ug : (𝓝 z).EventuallyEq b.u (b.g x)
⊢ ∀ᶠ (x : E) in 𝓝 z, b.u x = f x
Tactic:
exact ug.trans ((b.gf x).filter_mono (nhds_le_nhdsSet ⟨m, zs⟩))
Proof state after:
no goals
Theorem: Base.up
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
⊢ ∀ᶠ (z : E) in 𝓝ˢ (closure s), p b.u z
Tactic:
apply Filter.eventually_of_mem (b.ot.mem_nhdsSet.mpr b.cover)
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
⊢ ∀ x ∈ b.t, p b.u x
Theorem: Base.up
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
⊢ ∀ x ∈ b.t, p b.u x
Tactic:
intro x m
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ b.t
⊢ p b.u x
Theorem: Base.up
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ b.t
⊢ p b.u x
Tactic:
refine b.congr (b.gp (b.y m) (b.yt m)) ?_
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ b.t
⊢ (𝓝 x).EventuallyEq (b.g (b.y m)) b.u
Theorem: Base.up
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ b.t
⊢ (𝓝 x).EventuallyEq (b.g (b.y m)) b.u
Tactic:
exact ((b.ug _).eventuallyEq_of_mem ((b.ot.inter isOpen_ball).mem_nhds ⟨m, b.yt m⟩)).symm
Proof state after:
no goals
Theorem: Set.Nonempty.left_invCoe
Proof state before:
X : Type
s : Set X
ne : s.Nonempty
⊢ ∀ (x : ↑s), ne.invCoe ↑x = x
Tactic:
intro ⟨x, m⟩
Proof state after:
X : Type
s : Set X
ne : s.Nonempty
x : X
m : x ∈ s
⊢ ne.invCoe ↑⟨x, m⟩ = ⟨x, m⟩
Theorem: Set.Nonempty.left_invCoe
Proof state before:
X : Type
s : Set X
ne : s.Nonempty
x : X
m : x ∈ s
⊢ ne.invCoe ↑⟨x, m⟩ = ⟨x, m⟩
Tactic:
simp only [Set.Nonempty.invCoe, Subtype.coe_mk, m, dif_pos]
Proof state after:
no goals
Theorem: Set.Nonempty.right_invCoe
Proof state before:
X : Type
s : Set X
ne : s.Nonempty
⊢ ∀ x ∈ s, ↑(ne.invCoe x) = x
Tactic:
intro x m
Proof state after:
X : Type
s : Set X
ne : s.Nonempty
x : X
m : x ∈ s
⊢ ↑(ne.invCoe x) = x
Theorem: Set.Nonempty.right_invCoe
Proof state before:
X : Type
s : Set X
ne : s.Nonempty
x : X
m : x ∈ s
⊢ ↑(ne.invCoe x) = x
Tactic:
simp only [Set.Nonempty.invCoe, m, dif_pos, Subtype.coe_mk]
Proof state after:
no goals
Theorem: Set.Nonempty.continuousOn_invCoe
Proof state before:
X : Type
s : Set X
ne : s.Nonempty
inst✝ : TopologicalSpace X
⊢ ContinuousOn ne.invCoe s
Tactic:
rw [embedding_subtype_val.continuousOn_iff]
Proof state after:
X : Type
s : Set X
ne : s.Nonempty
inst✝ : TopologicalSpace X
⊢ ContinuousOn (Subtype.val ∘ ne.invCoe) s