internlm/Lean-Github huggingface dataset:
Theorem: on_subdisk
Proof state before:
case h.intro.intro.intro.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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
have c0e : c0' ∈ closedBall c0 e :=
  _root_.trans tr (Metric.closedBall_subset_closedBall (min_le_right _ _))
    (Metric.mem_ball_self tp)
Proof state after:
case h.intro.intro.intro.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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Theorem: on_subdisk
Proof state before:
case h.intro.intro.intro.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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
have fb : ∀ z, z ∈ ball c0' t ×ˢ ball c1 r → ‖f z‖ ≤ b := by
  intro z zs; rw [Set.mem_prod] at zs
  have zb := _root_.trans ts s's zs.left
  rw [← hS] at zb
  simp only [Metric.mem_ball, Metric.mem_closedBall, le_min_iff, Set.mem_setOf_eq] at zb zs
  have zb' := zb.right z.snd zs.right.le
  simp only [Prod.mk.eta] at zb'; exact zb'
Proof state after:
case h.intro.intro.intro.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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
fb : ∀ z ∈ ball c0' t ×ˢ ball c1 r, ‖f z‖ ≤ ↑b
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Theorem: on_subdisk
Proof state before:
case h.intro.intro.intro.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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
fb : ∀ z ∈ ball c0' t ×ˢ ball c1 r, ‖f z‖ ≤ ↑b
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
use t, tp, c0e
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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
fb : ∀ z ∈ ball c0' t ×ˢ ball c1 r, ‖f z‖ ≤ ↑b
⊢ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Theorem: on_subdisk
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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
fb : ∀ z ∈ ball c0' t ×ˢ ball c1 r, ‖f z‖ ≤ ↑b
⊢ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
refine of_bounded (h.mono ?_) (IsOpen.prod isOpen_ball isOpen_ball) 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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
fb : ∀ z ∈ ball c0' t ×ˢ ball c1 r, ‖f z‖ ≤ ↑b
⊢ ball c0' t ×ˢ ball c1 r ⊆ closedBall (c0, c1) r
Theorem: on_subdisk
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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
fb : ∀ z ∈ ball c0' t ×ˢ ball c1 r, ‖f z‖ ≤ ↑b
⊢ ball c0' t ×ˢ ball c1 r ⊆ closedBall (c0, c1) r
Tactic:
rw [← closedBall_prod_same]
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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
fb : ∀ z ∈ ball c0' t ×ˢ ball c1 r, ‖f z‖ ≤ ↑b
⊢ ball c0' t ×ˢ ball c1 r ⊆ closedBall c0 r ×ˢ closedBall c1 r
Theorem: on_subdisk
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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
fb : ∀ z ∈ ball c0' t ×ˢ ball c1 r, ‖f z‖ ≤ ↑b
⊢ ball c0' t ×ˢ ball c1 r ⊆ closedBall c0 r ×ˢ closedBall c1 r
Tactic:
exact Set.prod_mono (_root_.trans tr esub) Metric.ball_subset_closedBall
Proof state after:
no goals
Theorem: on_subdisk
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
⊢ ∀ (b : ℕ), IsClosed (S b)
Tactic:
intro b
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ IsClosed (S b)
Theorem: on_subdisk
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ IsClosed (S b)
Tactic:
rw [← hS]
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ IsClosed ((fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) b)
Theorem: on_subdisk
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ IsClosed ((fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) b)
Tactic:
simp only [← forall_const_and_distrib]
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ IsClosed {z0 | ∀ (x : ℂ), z0 ∈ closedBall c0 re ∧ (x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ ↑b)}
Theorem: on_subdisk
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ IsClosed {z0 | ∀ (x : ℂ), z0 ∈ closedBall c0 re ∧ (x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ ↑b)}
Tactic:
rw [Set.setOf_forall]
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ IsClosed (⋂ i, {x | x ∈ closedBall c0 re ∧ (i ∈ closedBall c1 r → ‖f (x, i)‖ ≤ ↑b)})
Theorem: on_subdisk
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ IsClosed (⋂ i, {x | x ∈ closedBall c0 re ∧ (i ∈ closedBall c1 r → ‖f (x, i)‖ ≤ ↑b)})
Tactic:
apply isClosed_iInter
Proof state after:
case h
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ ∀ (i : ℂ), IsClosed {x | x ∈ closedBall c0 re ∧ (i ∈ closedBall c1 r → ‖f (x, i)‖ ≤ ↑b)}
Theorem: on_subdisk
Proof state before:
case h
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ ∀ (i : ℂ), IsClosed {x | x ∈ closedBall c0 re ∧ (i ∈ closedBall c1 r → ‖f (x, i)‖ ≤ ↑b)}
Tactic:
intro z1
Proof state after:
case h
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ (z1 ∈ closedBall c1 r → ‖f (x, z1)‖ ≤ ↑b)}
Theorem: on_subdisk
Proof state before:
case h
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ (z1 ∈ closedBall c1 r → ‖f (x, z1)‖ ≤ ↑b)}
Tactic:
by_cases z1r : z1 ∉ closedBall c1 r
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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∉ closedBall c1 r
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ (z1 ∈ closedBall c1 r → ‖f (x, z1)‖ ≤ ↑b)}

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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : ¬z1 ∉ closedBall c1 r
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ (z1 ∈ closedBall c1 r → ‖f (x, z1)‖ ≤ ↑b)}
Theorem: on_subdisk
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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∉ closedBall c1 r
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ (z1 ∈ closedBall c1 r → ‖f (x, z1)‖ ≤ ↑b)}
Tactic:
simp only [z1r, false_imp_iff, and_true_iff, Set.setOf_mem_eq, Metric.isClosed_ball]
Proof state after:
no goals
Theorem: on_subdisk
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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : ¬z1 ∉ closedBall c1 r
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ (z1 ∈ closedBall c1 r → ‖f (x, z1)‖ ≤ ↑b)}
Tactic:
rw [Set.not_not_mem] at z1r
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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∈ closedBall c1 r
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ (z1 ∈ closedBall c1 r → ‖f (x, z1)‖ ≤ ↑b)}
Theorem: on_subdisk
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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∈ closedBall c1 r
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ (z1 ∈ closedBall c1 r → ‖f (x, z1)‖ ≤ ↑b)}
Tactic:
simp only [z1r, true_imp_iff]
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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∈ closedBall c1 r
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ ‖f (x, z1)‖ ≤ ↑b}
Theorem: on_subdisk
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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∈ closedBall c1 r
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ ‖f (x, z1)‖ ≤ ↑b}
Tactic:
refine ContinuousOn.isClosed_le Metric.isClosed_ball ?_ continuousOn_const
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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∈ closedBall c1 r
⊢ ContinuousOn (fun x => ‖f (x, z1)‖) (closedBall c0 re)
Theorem: on_subdisk
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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∈ closedBall c1 r
⊢ ContinuousOn (fun x => ‖f (x, z1)‖) (closedBall c0 re)
Tactic:
apply ContinuousOn.norm
Proof state after:
case neg.h
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∈ closedBall c1 r
⊢ ContinuousOn (fun x => f (x, z1)) (closedBall c0 re)
Theorem: on_subdisk
Proof state before:
case neg.h
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∈ closedBall c1 r
⊢ ContinuousOn (fun x => f (x, z1)) (closedBall c0 re)
Tactic:
exact ContinuousOn.mono (h.on0 z1r).continuousOn esub
Proof state after:
no goals