internlm/Lean-Github huggingface dataset:
Theorem: hxSegBallInterSeg
Proof state before:
case h.right.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε
Tactic:
rw [Set.subset_inter_iff]
Proof state after:
case h.right.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∧ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ Metric.ball x ε
Theorem: hxSegBallInterSeg
Proof state before:
case h.right.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∧ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ Metric.ball x ε
Tactic:
constructor
Proof state after:
case h.right.left.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2

case h.right.left.right
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ Metric.ball x ε
Theorem: hxSegBallInterSeg
Proof state before:
case h.right.left.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2
Tactic:
have := @convex_openSegment ℝ _ _ _ _ x1 x2
Proof state after:
case h.right.left.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
this : Convex ℝ (openSegment ℝ x1 x2)
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2
Theorem: hxSegBallInterSeg
Proof state before:
case h.right.left.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
this : Convex ℝ (openSegment ℝ x1 x2)
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2
Tactic:
rw [convex_iff_segment_subset] at this
Proof state after:
case h.right.left.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
this : ∀ ⦃x : E⦄, x ∈ openSegment ℝ x1 x2 → ∀ ⦃y : E⦄, y ∈ openSegment ℝ x1 x2 → segment ℝ x y ⊆ openSegment ℝ x1 x2
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2
Theorem: hxSegBallInterSeg
Proof state before:
case h.right.left.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
this : ∀ ⦃x : E⦄, x ∈ openSegment ℝ x1 x2 → ∀ ⦃y : E⦄, y ∈ openSegment ℝ x1 x2 → segment ℝ x y ⊆ openSegment ℝ x1 x2
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2
Tactic:
apply this <;> clear this <;> rw [←htt] <;>
rw [@add_comm _ _ x1, ←add_assoc, ← add_smul, @add_comm _ _ _ t, openSegment_eq_image']
Proof state after:
case h.right.left.left.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ (t + t1) • v + x1 ∈ (fun θ => x1 + θ • (x2 - x1)) '' Set.Ioo 0 1

case h.right.left.left.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ (t + t2) • v + x1 ∈ (fun θ => x1 + θ • (x2 - x1)) '' Set.Ioo 0 1
Theorem: hxSegBallInterSeg
Proof state before:
case h.right.left.left.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ (t + t1) • v + x1 ∈ (fun θ => x1 + θ • (x2 - x1)) '' Set.Ioo 0 1
Tactic:
exact ⟨ t + t1,
  ⟨ lt_of_le_of_lt' (by linarith [min_le_left t (ε/norm v)] : t -t/2 ≤ t -(min t (ε /norm v)/2))
    (by linarith [ht.1]), lt_trans (add_lt_of_neg_right t ht1) ht.2 ⟩,
  by unfold_let v; simp only [ge_iff_le]; rw [add_comm, @add_comm _ _ t t1, sub_eq_neg_add] ⟩
Proof state after:
no goals
Theorem: hxSegBallInterSeg
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ t - t / 2 ≤ t - min t (ε / ‖v‖) / 2
Tactic:
linarith [min_le_left t (ε/norm v)]
Proof state after:
no goals
Theorem: hxSegBallInterSeg
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ 0 < t - t / 2
Tactic:
linarith [ht.1]
Proof state after:
no goals
Theorem: hxSegBallInterSeg
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ (fun θ => x1 + θ • (x2 - x1)) (t + t1) = (t + t1) • v + x1
Tactic:
unfold_let v
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ (fun θ => x1 + θ • (x2 - x1)) (t + t1) = (t + t1) • (x2 - x1) + x1
Theorem: hxSegBallInterSeg
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ (fun θ => x1 + θ • (x2 - x1)) (t + t1) = (t + t1) • (x2 - x1) + x1
Tactic:
simp only [ge_iff_le]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ x1 + (t + t1) • (x2 - x1) = (t + t1) • (x2 - x1) + x1
Theorem: hxSegBallInterSeg
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ x1 + (t + t1) • (x2 - x1) = (t + t1) • (x2 - x1) + x1
Tactic:
rw [add_comm, @add_comm _ _ t t1, sub_eq_neg_add]
Proof state after:
no goals
Theorem: hxSegBallInterSeg
Proof state before:
case h.right.left.left.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ (t + t2) • v + x1 ∈ (fun θ => x1 + θ • (x2 - x1)) '' Set.Ioo 0 1
Tactic:
refine ⟨ t + t2,
  ⟨ lt_trans ht.1 (by linarith [ht2pos] : t < t + (min (1 - t) (ε / ‖x2 - x1‖) / 2)), ?_ ⟩,
  by simp only [ge_iff_le] ;rw [add_comm] ⟩
Proof state after:
case h.right.left.left.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ t + t2 < 1
Theorem: hxSegBallInterSeg
Proof state before:
case h.right.left.left.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ t + t2 < 1
Tactic:
exact lt_of_lt_of_le' (by linarith [ht.2]) (by linarith [min_le_left (1 - t) ((ε / ‖x2 - x1‖))]
  : t + min (1 - t) (ε / ‖x2 - x1‖) / 2 ≤ t + ((1 - t) / 2))
Proof state after:
no goals
Theorem: hxSegBallInterSeg
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ t < t + min (1 - t) (ε / ‖x2 - x1‖) / 2
Tactic:
linarith [ht2pos]
Proof state after:
no goals
Theorem: hxSegBallInterSeg
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ (fun θ => x1 + θ • (x2 - x1)) (t + t2) = (t + t2) • v + x1
Tactic:
simp only [ge_iff_le]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ x1 + (t + t2) • (x2 - x1) = (t + t2) • v + x1
Theorem: hxSegBallInterSeg
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ x1 + (t + t2) • (x2 - x1) = (t + t2) • v + x1
Tactic:
rw [add_comm]
Proof state after:
no goals
Theorem: hxSegBallInterSeg
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ t + (1 - t) / 2 < 1
Tactic:
linarith [ht.2]
Proof state after:
no goals
Theorem: hxSegBallInterSeg
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ t + min (1 - t) (ε / ‖x2 - x1‖) / 2 ≤ t + (1 - t) / 2
Tactic:
linarith [min_le_left (1 - t) ((ε / ‖x2 - x1‖))]
Proof state after:
no goals
Theorem: hxSegBallInterSeg
Proof state before:
case h.right.left.right
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ Metric.ball x ε
Tactic:
clear ht hxseg' hne
Proof state after:
case h.right.left.right
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
t : ℝ
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ Metric.ball x ε
Theorem: hxSegBallInterSeg
Proof state before:
case h.right.left.right
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
t : ℝ
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ Metric.ball x ε
Tactic:
rw [← half_lt_self_iff] at hε
Proof state after:
case h.right.left.right
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : ε / 2 < ε
t : ℝ
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ Metric.ball x ε
Theorem: hxSegBallInterSeg
Proof state before:
case h.right.left.right
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : ε / 2 < ε
t : ℝ
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ Metric.ball x ε
Tactic:
apply (convex_iff_segment_subset.mp <| convex_ball x ε ) <;> rw [Metric.mem_ball] <;> norm_num <;> unfold_let
Proof state after:
case h.right.left.right.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : ε / 2 < ε
t : ℝ
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ ‖-(min t (ε / ‖x2 - x1‖) / 2) • (x2 - x1)‖ < ε

case h.right.left.right.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : ε / 2 < ε
t : ℝ
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ ‖(min (1 - t) (ε / ‖x2 - x1‖) / 2) • (x2 - x1)‖ < ε
Theorem: hxSegBallInterSeg
Proof state before:
case h.right.left.right.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : ε / 2 < ε
t : ℝ
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ ‖-(min t (ε / ‖x2 - x1‖) / 2) • (x2 - x1)‖ < ε

case h.right.left.right.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : ε / 2 < ε
t : ℝ
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ ‖(min (1 - t) (ε / ‖x2 - x1‖) / 2) • (x2 - x1)‖ < ε
Tactic:
simp
Proof state after:
case h.right.left.right.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : ε / 2 < ε
t : ℝ
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ ‖(min t (ε / ‖x2 - x1‖) / 2) • (x2 - x1)‖ < ε

case h.right.left.right.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : ε / 2 < ε
t : ℝ
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ ‖(min (1 - t) (ε / ‖x2 - x1‖) / 2) • (x2 - x1)‖ < ε