Theorem: of_bounded (Ray/Hartogs/Hartogs.lean)

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
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

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
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

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
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

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
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

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⟩
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

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]
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) < ε

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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)))
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

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]
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals