internlm/Lean-Github huggingface dataset:
Theorem: ContinuousOn.partialSups
Proof state before:
case succ
A : Type
inst✝ : TopologicalSpace A
f : ℕ → A → ℝ
s : Set A
fc : ∀ (n : ℕ), ContinuousOn (f n) s
n : ℕ
h : ContinuousOn (fun x => (_root_.partialSups fun k => f k x) n) s
⊢ ContinuousOn (fun x => (_root_.partialSups fun k => f k x) (n + 1)) s
Tactic:
simp
Proof state after:
case succ
A : Type
inst✝ : TopologicalSpace A
f : ℕ → A → ℝ
s : Set A
fc : ∀ (n : ℕ), ContinuousOn (f n) s
n : ℕ
h : ContinuousOn (fun x => (_root_.partialSups fun k => f k x) n) s
⊢ ContinuousOn (fun x => (_root_.partialSups fun k => f k x) n ⊔ f (n + 1) x) s
Theorem: ContinuousOn.partialSups
Proof state before:
case succ
A : Type
inst✝ : TopologicalSpace A
f : ℕ → A → ℝ
s : Set A
fc : ∀ (n : ℕ), ContinuousOn (f n) s
n : ℕ
h : ContinuousOn (fun x => (_root_.partialSups fun k => f k x) n) s
⊢ ContinuousOn (fun x => (_root_.partialSups fun k => f k x) n ⊔ f (n + 1) x) s
Tactic:
exact ContinuousOn.max h (fc _)
Proof state after:
no goals
Theorem: Har.flip
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
⊢ ∀ (c0 c1 : ℂ), (c0, c1) ∈ swap '' s → AnalyticAt ℂ (fun z0 => (f ∘ swap) (z0, c1)) c0
Tactic:
intro c0 c1 cs
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c0, c1) ∈ swap '' s
⊢ AnalyticAt ℂ (fun z0 => (f ∘ swap) (z0, c1)) c0
Theorem: Har.flip
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c0, c1) ∈ swap '' s
⊢ AnalyticAt ℂ (fun z0 => (f ∘ swap) (z0, c1)) c0
Tactic:
simp only [Function.comp_apply, Prod.swap_prod_mk]
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c0, c1) ∈ swap '' s
⊢ AnalyticAt ℂ (fun z0 => f (c1, z0)) c0
Theorem: Har.flip
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c0, c1) ∈ swap '' s
⊢ AnalyticAt ℂ (fun z0 => f (c1, z0)) c0
Tactic:
rw [swap_mem] at cs
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c1, c0) ∈ s
⊢ AnalyticAt ℂ (fun z0 => f (c1, z0)) c0
Theorem: Har.flip
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c1, c0) ∈ s
⊢ AnalyticAt ℂ (fun z0 => f (c1, z0)) c0
Tactic:
exact h.fa1 c1 c0 cs
Proof state after:
no goals
Theorem: Har.flip
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
⊢ ∀ (c0 c1 : ℂ), (c0, c1) ∈ swap '' s → AnalyticAt ℂ (fun z1 => (f ∘ swap) (c0, z1)) c1
Tactic:
intro c0 c1 cs
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c0, c1) ∈ swap '' s
⊢ AnalyticAt ℂ (fun z1 => (f ∘ swap) (c0, z1)) c1
Theorem: Har.flip
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c0, c1) ∈ swap '' s
⊢ AnalyticAt ℂ (fun z1 => (f ∘ swap) (c0, z1)) c1
Tactic:
simp only [Function.comp_apply, Prod.swap_prod_mk]
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c0, c1) ∈ swap '' s
⊢ AnalyticAt ℂ (fun z1 => f (z1, c0)) c1
Theorem: Har.flip
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c0, c1) ∈ swap '' s
⊢ AnalyticAt ℂ (fun z1 => f (z1, c0)) c1
Tactic:
rw [swap_mem] at cs
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c1, c0) ∈ s
⊢ AnalyticAt ℂ (fun z1 => f (z1, c0)) c1
Theorem: Har.flip
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0✝ c0' c1✝ z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f s
c0 c1 : ℂ
cs : (c1, c0) ∈ s
⊢ AnalyticAt ℂ (fun z1 => f (z1, c0)) c1
Tactic:
exact h.fa0 c1 c0 cs
Proof state after:
no goals
Theorem: Har.on0
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
z1r : z1 ∈ closedBall c1 r
⊢ AnalyticOn ℂ (fun z0 => f (z0, z1)) (closedBall c0 r)
Tactic:
intro z0 z0s
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0✝ z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
z1r : z1 ∈ closedBall c1 r
z0 : ℂ
z0s : z0 ∈ closedBall c0 r
⊢ AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
Theorem: Har.on0
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0✝ z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
z1r : z1 ∈ closedBall c1 r
z0 : ℂ
z0s : z0 ∈ closedBall c0 r
⊢ AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
Tactic:
apply h.fa0 z0 z1
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0✝ z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
z1r : z1 ∈ closedBall c1 r
z0 : ℂ
z0s : z0 ∈ closedBall c0 r
⊢ (z0, z1) ∈ closedBall (c0, c1) r
Theorem: Har.on0
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0✝ z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
z1r : z1 ∈ closedBall c1 r
z0 : ℂ
z0s : z0 ∈ closedBall c0 r
⊢ (z0, z1) ∈ closedBall (c0, c1) r
Tactic:
rw [← closedBall_prod_same]
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0✝ z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
z1r : z1 ∈ closedBall c1 r
z0 : ℂ
z0s : z0 ∈ closedBall c0 r
⊢ (z0, z1) ∈ closedBall c0 r ×ˢ closedBall c1 r
Theorem: Har.on0
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0✝ z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
z1r : z1 ∈ closedBall c1 r
z0 : ℂ
z0s : z0 ∈ closedBall c0 r
⊢ (z0, z1) ∈ closedBall c0 r ×ˢ closedBall c1 r
Tactic:
simp only [Set.prod_mk_mem_set_prod_eq, Metric.mem_closedBall] at z0s ⊢
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0✝ z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
z1r : z1 ∈ closedBall c1 r
z0 : ℂ
z0s : dist z0 c0 ≤ r
⊢ dist z0 c0 ≤ r ∧ dist z1 c1 ≤ r
Theorem: Har.on0
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0✝ z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
z1r : z1 ∈ closedBall c1 r
z0 : ℂ
z0s : dist z0 c0 ≤ r
⊢ dist z0 c0 ≤ r ∧ dist z1 c1 ≤ r
Tactic:
exact ⟨z0s, z1r⟩
Proof state after:
no goals
Theorem: Har.on1
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
z0r : z0 ∈ closedBall c0 r
⊢ AnalyticOn ℂ (fun z1 => f (z0, z1)) (closedBall c1 r)
Tactic:
intro z1 z1s
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
z0r : z0 ∈ closedBall c0 r
z1 : ℂ
z1s : z1 ∈ closedBall c1 r
⊢ AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
Theorem: Har.on1
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
z0r : z0 ∈ closedBall c0 r
z1 : ℂ
z1s : z1 ∈ closedBall c1 r
⊢ AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
Tactic:
apply h.fa1 z0 z1
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
z0r : z0 ∈ closedBall c0 r
z1 : ℂ
z1s : z1 ∈ closedBall c1 r
⊢ (z0, z1) ∈ closedBall (c0, c1) r
Theorem: Har.on1
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
z0r : z0 ∈ closedBall c0 r
z1 : ℂ
z1s : z1 ∈ closedBall c1 r
⊢ (z0, z1) ∈ closedBall (c0, c1) r
Tactic:
rw [← closedBall_prod_same]
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
z0r : z0 ∈ closedBall c0 r
z1 : ℂ
z1s : z1 ∈ closedBall c1 r
⊢ (z0, z1) ∈ closedBall c0 r ×ˢ closedBall c1 r
Theorem: Har.on1
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
z0r : z0 ∈ closedBall c0 r
z1 : ℂ
z1s : z1 ∈ closedBall c1 r
⊢ (z0, z1) ∈ closedBall c0 r ×ˢ closedBall c1 r
Tactic:
simp only [Set.prod_mk_mem_set_prod_eq, Metric.mem_closedBall] at z1s ⊢
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
z0r : z0 ∈ closedBall c0 r
z1 : ℂ
z1s : dist z1 c1 ≤ r
⊢ dist z0 c0 ≤ r ∧ dist z1 c1 ≤ r
Theorem: Har.on1
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
z0r : z0 ∈ closedBall c0 r
z1 : ℂ
z1s : dist z1 c1 ≤ r
⊢ dist z0 c0 ≤ r ∧ dist z1 c1 ≤ r
Tactic:
exact ⟨z0r, z1s⟩
Proof state after:
no goals
Theorem: Bounded.dist0
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b✝ e✝ : ℝ
h : Har f s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
generalize hu : min (r / 2) (e * r / b / 24) = u
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b✝ e✝ : ℝ
h : Har f s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
hu : min (r / 2) (e * r / b / 24) = u
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Theorem: Bounded.dist0
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b✝ e✝ : ℝ
h : Har f s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
hu : min (r / 2) (e * r / b / 24) = u
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
rw [hu] at wz
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b✝ e✝ : ℝ
h : Har f s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Theorem: Bounded.dist0
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b✝ e✝ : ℝ
h : Har f s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
have up : 0 < u := by
  rw [← hu]; simp only [gt_iff_lt, lt_min_iff]
  exact ⟨by bound, by bound⟩
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b✝ e✝ : ℝ
h : Har f s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Theorem: Bounded.dist0
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b✝ e✝ : ℝ
h : Har f s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
have ur : u ≤ r / 2 := by rw [← hu]; exact min_le_left _ _
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b✝ e✝ : ℝ
h : Har f s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Theorem: Bounded.dist0
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b✝ e✝ : ℝ
h : Har f s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
have ue : 6 * b / r * u ≤ e / 4 := by
  rw [← hu]
  calc 6 * b / r * min (r / 2) (e * r / b / 24)
    _ ≤ 6 * b / r * (e * r / b / 24) := by bound
    _ = b / b * (r / r) * (e / 4) := by ring
    _ = e / 4 := by field_simp [bp.ne', rp.ne']
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b✝ e✝ : ℝ
h : Har f s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Theorem: Bounded.dist0
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b✝ e✝ : ℝ
h : Har f s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
rw [ball_prod_same'] at rs
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b✝ e✝ : ℝ
h : Har f s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Theorem: Bounded.dist0
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b✝ e✝ : ℝ
h : Har f s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
rw [← Metric.mem_ball, ball_prod_same', Set.mem_prod] at wz
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b✝ e✝ : ℝ
h : Har f s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : w.1 ∈ ball z.1 u ∧ w.2 ∈ ball z.2 u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Theorem: Bounded.dist0
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b✝ e✝ : ℝ
h : Har f s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : w.1 ∈ ball z.1 u ∧ w.2 ∈ ball z.2 u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
have d : DifferentiableOn ℂ (fun t ↦ f (t, w.snd)) (ball z.fst (r / 2)) := by
  intro t ts; refine (h.fa0 t w.snd ?_).differentiableWithinAt
  exact rs (Set.mk_mem_prod ts (Metric.ball_subset_ball ur wz.right))
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b✝ e✝ : ℝ
h : Har f s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : w.1 ∈ ball z.1 u ∧ w.2 ∈ ball z.2 u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
d : DifferentiableOn ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2))
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Theorem: Bounded.dist0
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b✝ e✝ : ℝ
h : Har f s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : w.1 ∈ ball z.1 u ∧ w.2 ∈ ball z.2 u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
d : DifferentiableOn ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2))
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
have wf : w.fst ∈ ball z.fst (r / 2) := Metric.ball_subset_ball ur wz.left
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b✝ e✝ : ℝ
h : Har f s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : w.1 ∈ ball z.1 u ∧ w.2 ∈ ball z.2 u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
d : DifferentiableOn ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2))
wf : w.1 ∈ ball z.1 (r / 2)
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4