internlm/Lean-Github huggingface dataset:
Theorem: Bounded.dist1
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
rr : dist w z ≤ r / 2
⊢ r / 2 + dist w z ≤ r / 2 + r / 2

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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
rr : dist w z ≤ r / 2
⊢ r / 2 + r / 2 ≤ r
Tactic:
linarith
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
rr : dist w z ≤ r / 2
⊢ r / 2 + r / 2 ≤ r
Theorem: Bounded.dist1
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
rr : dist w z ≤ r / 2
⊢ r / 2 + r / 2 ≤ r
Tactic:
ring_nf
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
rr : dist w z ≤ r / 2
⊢ r ≤ r
Theorem: Bounded.dist1
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
rr : dist w z ≤ r / 2
⊢ r ≤ r
Tactic:
apply le_refl
Proof state after:
no goals
Theorem: Bounded.dist1
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
wrs : ball w (r / 2) ⊆ s
⊢ ball w.swap (r / 2) ⊆ swap '' s
Tactic:
rw [ball_swap]
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
wrs : ball w (r / 2) ⊆ s
⊢ swap '' ball w (r / 2) ⊆ swap '' s
Theorem: Bounded.dist1
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
wrs : ball w (r / 2) ⊆ s
⊢ swap '' ball w (r / 2) ⊆ swap '' s
Tactic:
exact Set.image_subset _ wrs
Proof state after:
no goals
Theorem: Bounded.dist1
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
wrs : ball w (r / 2) ⊆ s
rs' : ball w.swap (r / 2) ⊆ swap '' s
⊢ dist z.swap w.swap < min (r / 2) (e * r / b / 24)
Tactic:
rwa [dist_swap, dist_comm]
Proof state after:
no goals
Theorem: of_bounded
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
⊢ AnalyticOn ℂ f s
Tactic:
suffices c : ContinuousOn f s by exact osgood o c h.fa0 h.fa1
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
⊢ ContinuousOn f s
Theorem: of_bounded
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
⊢ ContinuousOn f s
Tactic:
by_cases bp : b ≤ 0
Proof state after:
case pos
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : b ≤ 0
⊢ ContinuousOn f s

case neg
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : ¬b ≤ 0
⊢ ContinuousOn f s
Theorem: of_bounded
Proof state before:
case neg
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : ¬b ≤ 0
⊢ ContinuousOn f s
Tactic:
simp only [not_le] at bp
Proof state after:
case neg
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
⊢ ContinuousOn f s
Theorem: of_bounded
Proof state before:
case neg
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
⊢ ContinuousOn f s
Tactic:
intro z zs
Proof state after:
case neg
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
⊢ ContinuousWithinAt f s z
Theorem: of_bounded
Proof state before:
case neg
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
⊢ ContinuousWithinAt f s z
Tactic:
rcases Metric.isOpen_iff.mp o z zs with ⟨r, rp, rs⟩
Proof state after:
case neg.intro.intro
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
⊢ ContinuousWithinAt f s z
Theorem: of_bounded
Proof state before:
case neg.intro.intro
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
⊢ ContinuousWithinAt f s z
Tactic:
rw [Metric.continuousWithinAt_iff]
Proof state after:
case neg.intro.intro
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
⊢ ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ × ℂ}, x ∈ s → dist x z < δ → dist (f x) (f z) < ε
Theorem: of_bounded
Proof state before:
case neg.intro.intro
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
⊢ ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ × ℂ}, x ∈ s → dist x z < δ → dist (f x) (f z) < ε
Tactic:
intro e ep
Proof state after:
case neg.intro.intro
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
e : ℝ
ep : e > 0
⊢ ∃ δ > 0, ∀ {x : ℂ × ℂ}, x ∈ s → dist x z < δ → dist (f x) (f z) < e
Theorem: of_bounded
Proof state before:
case neg.intro.intro
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
e : ℝ
ep : e > 0
⊢ ∃ δ > 0, ∀ {x : ℂ × ℂ}, x ∈ s → dist x z < δ → dist (f x) (f z) < e
Tactic:
have up : min (r / 2) (e * r / b / 24) > 0 := by bound
Proof state after:
case neg.intro.intro
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
e : ℝ
ep : e > 0
up : min (r / 2) (e * r / b / 24) > 0
⊢ ∃ δ > 0, ∀ {x : ℂ × ℂ}, x ∈ s → dist x z < δ → dist (f x) (f z) < e
Theorem: of_bounded
Proof state before:
case neg.intro.intro
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
e : ℝ
ep : e > 0
up : min (r / 2) (e * r / b / 24) > 0
⊢ ∃ δ > 0, ∀ {x : ℂ × ℂ}, x ∈ s → dist x z < δ → dist (f x) (f z) < e
Tactic:
use min (r / 2) (e * r / b / 24), up
Proof state after:
case right
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
e : ℝ
ep : e > 0
up : min (r / 2) (e * r / b / 24) > 0
⊢ ∀ {x : ℂ × ℂ}, x ∈ s → dist x z < min (r / 2) (e * r / b / 24) → dist (f x) (f z) < e
Theorem: of_bounded
Proof state before:
case right
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
e : ℝ
ep : e > 0
up : min (r / 2) (e * r / b / 24) > 0
⊢ ∀ {x : ℂ × ℂ}, x ∈ s → dist x z < min (r / 2) (e * r / b / 24) → dist (f x) (f z) < e
Tactic:
intro w _ wz
Proof state after:
case right
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
e : ℝ
ep : e > 0
up : min (r / 2) (e * r / b / 24) > 0
w : ℂ × ℂ
a✝ : w ∈ s
wz : dist w z < min (r / 2) (e * r / b / 24)
⊢ dist (f w) (f z) < e
Theorem: of_bounded
Proof state before:
case right
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
e : ℝ
ep : e > 0
up : min (r / 2) (e * r / b / 24) > 0
w : ℂ × ℂ
a✝ : w ∈ s
wz : dist w z < min (r / 2) (e * r / b / 24)
⊢ dist (f w) (f z) < e
Tactic:
have s0 : dist (f w) (f (z.fst, w.snd)) ≤ e / 4 :=
  Bounded.dist0 h bp ep rp (_root_.trans (Metric.ball_subset_ball (by linarith)) rs) wz fb
Proof state after:
case right
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
e : ℝ
ep : e > 0
up : min (r / 2) (e * r / b / 24) > 0
w : ℂ × ℂ
a✝ : w ∈ s
wz : dist w z < min (r / 2) (e * r / b / 24)
s0 : dist (f w) (f (z.1, w.2)) ≤ e / 4
⊢ dist (f w) (f z) < e
Theorem: of_bounded
Proof state before:
case right
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
e : ℝ
ep : e > 0
up : min (r / 2) (e * r / b / 24) > 0
w : ℂ × ℂ
a✝ : w ∈ s
wz : dist w z < min (r / 2) (e * r / b / 24)
s0 : dist (f w) (f (z.1, w.2)) ≤ e / 4
⊢ dist (f w) (f z) < e
Tactic:
have s1 : dist (f (z.fst, w.snd)) (f z) ≤ e / 4 := Bounded.dist1 h bp ep rp rs wz fb
Proof state after:
case right
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
e : ℝ
ep : e > 0
up : min (r / 2) (e * r / b / 24) > 0
w : ℂ × ℂ
a✝ : w ∈ s
wz : dist w z < min (r / 2) (e * r / b / 24)
s0 : dist (f w) (f (z.1, w.2)) ≤ e / 4
s1 : dist (f (z.1, w.2)) (f z) ≤ e / 4
⊢ dist (f w) (f z) < e
Theorem: of_bounded
Proof state before:
case right
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
e : ℝ
ep : e > 0
up : min (r / 2) (e * r / b / 24) > 0
w : ℂ × ℂ
a✝ : w ∈ s
wz : dist w z < min (r / 2) (e * r / b / 24)
s0 : dist (f w) (f (z.1, w.2)) ≤ e / 4
s1 : dist (f (z.1, w.2)) (f z) ≤ e / 4
⊢ dist (f w) (f z) < e
Tactic:
calc dist (f w) (f z)
  _ ≤ dist (f w) (f (z.fst, w.snd)) + dist (f (z.fst, w.snd)) (f z) := dist_triangle _ _ _
  _ ≤ e / 4 + e / 4 := by linarith
  _ = e / 2 := by ring
  _ < e := by linarith
Proof state after:
no goals
Theorem: of_bounded
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
c : ContinuousOn f s
⊢ AnalyticOn ℂ f s
Tactic:
exact osgood o c h.fa0 h.fa1
Proof state after:
no goals
Theorem: of_bounded
Proof state before:
case pos
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : b ≤ 0
⊢ ContinuousOn f s
Tactic:
have fz : ∀ z, z ∈ s → f z = 0 := fun z zs ↦
  norm_eq_zero.mp (le_antisymm (_root_.trans (fb z zs) bp) (norm_nonneg (f z)))
Proof state after:
case pos
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : b ≤ 0
fz : ∀ z ∈ s, f z = 0
⊢ ContinuousOn f s
Theorem: of_bounded
Proof state before:
case pos
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : b ≤ 0
fz : ∀ z ∈ s, f z = 0
⊢ ContinuousOn f s
Tactic:
rw [continuousOn_congr fz]
Proof state after:
case pos
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : b ≤ 0
fz : ∀ z ∈ s, f z = 0
⊢ ContinuousOn (fun x => 0) s
Theorem: of_bounded
Proof state before:
case pos
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : b ≤ 0
fz : ∀ z ∈ s, f z = 0
⊢ ContinuousOn (fun x => 0) s
Tactic:
exact continuousOn_const
Proof state after:
no goals
Theorem: of_bounded
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
e : ℝ
ep : e > 0
⊢ min (r / 2) (e * r / b / 24) > 0
Tactic:
bound
Proof state after:
no goals
Theorem: of_bounded
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
e : ℝ
ep : e > 0
up : min (r / 2) (e * r / b / 24) > 0
w : ℂ × ℂ
a✝ : w ∈ s
wz : dist w z < min (r / 2) (e * r / b / 24)
⊢ r / 2 ≤ r
Tactic:
linarith
Proof state after:
no goals
Theorem: of_bounded
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
e : ℝ
ep : e > 0
up : min (r / 2) (e * r / b / 24) > 0
w : ℂ × ℂ
a✝ : w ∈ s
wz : dist w z < min (r / 2) (e * r / b / 24)
s0 : dist (f w) (f (z.1, w.2)) ≤ e / 4
s1 : dist (f (z.1, w.2)) (f z) ≤ e / 4
⊢ dist (f w) (f (z.1, w.2)) + dist (f (z.1, w.2)) (f z) ≤ e / 4 + e / 4
Tactic:
linarith
Proof state after:
no goals
Theorem: of_bounded
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
e : ℝ
ep : e > 0
up : min (r / 2) (e * r / b / 24) > 0
w : ℂ × ℂ
a✝ : w ∈ s
wz : dist w z < min (r / 2) (e * r / b / 24)
s0 : dist (f w) (f (z.1, w.2)) ≤ e / 4
s1 : dist (f (z.1, w.2)) (f z) ≤ e / 4
⊢ e / 4 + e / 4 = e / 2
Tactic:
ring
Proof state after:
no goals
Theorem: of_bounded
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
o : IsOpen s
b : ℝ
fb : ∀ z ∈ s, ‖f z‖ ≤ b
bp : 0 < b
z : ℂ × ℂ
zs : z ∈ s
r : ℝ
rp : r > 0
rs : ball z r ⊆ s
e : ℝ
ep : e > 0
up : min (r / 2) (e * r / b / 24) > 0
w : ℂ × ℂ
a✝ : w ∈ s
wz : dist w z < min (r / 2) (e * r / b / 24)
s0 : dist (f w) (f (z.1, w.2)) ≤ e / 4
s1 : dist (f (z.1, w.2)) (f z) ≤ e / 4
⊢ e / 2 < e
Tactic:
linarith
Proof state after:
no goals
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
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 : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
hU : (interior (⋃ k, f k)).Nonempty
⊢ ∃ k, (interior (f k)).Nonempty
Tactic:
set s := interior (⋃ k, f k)
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 : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
⊢ ∃ k, (interior (f k)).Nonempty
Theorem: NonemptyInterior.nonempty_interior_of_iUnion_of_closed
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 : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
⊢ ∃ k, (interior (f k)).Nonempty
Tactic:
set f' : Option B → Set A := fun k ↦
  match k with
  | none => sᶜ
  | some k => f k
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 : ℝ
A B : Type
inst✝² : TopologicalSpace A
inst✝¹ : BaireSpace A
inst✝ : Encodable B
f : B → Set A
hc : ∀ (k : B), IsClosed (f k)
s : Set A := interior (⋃ k, f k)
hU : s.Nonempty
f' : Option B → Set A :=
  fun k =>
    match k with
    | none => sᶜ
    | some k => f k
⊢ ∃ k, (interior (f k)).Nonempty