internlm/Lean-Github huggingface dataset:
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
hc : ∀ (b : ℕ), IsClosed (S b)
⊢ (interior (⋃ b, S b)).Nonempty
Tactic:
refine Set.nonempty_of_mem
    (mem_interior.mpr ⟨ball c0 re, ?_, Metric.isOpen_ball, Metric.mem_ball_self (lt_min rp ep)⟩)
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
hc : ∀ (b : ℕ), IsClosed (S b)
⊢ ball c0 re ⊆ ⋃ b, 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
hc : ∀ (b : ℕ), IsClosed (S b)
⊢ ball c0 re ⊆ ⋃ b, S b
Tactic:
rw [Set.subset_def]
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
hc : ∀ (b : ℕ), IsClosed (S b)
⊢ ∀ x ∈ ball c0 re, x ∈ ⋃ b, 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
hc : ∀ (b : ℕ), IsClosed (S b)
⊢ ∀ x ∈ ball c0 re, x ∈ ⋃ b, S b
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)
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)
z0 : ℂ
z0s : z0 ∈ ball c0 re
⊢ z0 ∈ ⋃ b, 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
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
⊢ z0 ∈ ⋃ b, S b
Tactic:
rw [Set.mem_iUnion]
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
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
⊢ ∃ i, z0 ∈ S i
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
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
⊢ ∃ i, z0 ∈ S i
Tactic:
have z0s' := esub (mem_open_closed 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)
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)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
⊢ ∃ i, z0 ∈ S i
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
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
⊢ ∃ i, z0 ∈ S i
Tactic:
rcases (isCompact_closedBall _ _).bddAbove_image (h.on1 z0s').continuousOn.norm with ⟨b, fb⟩
Proof state after:
case 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)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : b ∈ upperBounds ((fun x => ‖f (z0, x)‖) '' closedBall c1 r)
⊢ ∃ i, z0 ∈ S i
Theorem: on_subdisk
Proof state before:
case 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)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : b ∈ upperBounds ((fun x => ‖f (z0, x)‖) '' closedBall c1 r)
⊢ ∃ i, z0 ∈ S i
Tactic:
simp only [mem_upperBounds, Set.forall_mem_image] at fb
Proof state after:
case 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)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ ∃ i, z0 ∈ S i
Theorem: on_subdisk
Proof state before:
case 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)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ ∃ i, z0 ∈ S i
Tactic:
use Nat.ceil b
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
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ z0 ∈ S ⌈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
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ z0 ∈ S ⌈b⌉₊
Tactic:
rw [← hS]
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
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ z0 ∈ (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) ⌈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
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ z0 ∈ (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) ⌈b⌉₊
Tactic:
simp only [Set.mem_setOf]
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
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, 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
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑⌈b⌉₊
Tactic:
refine ⟨mem_open_closed z0s, ?_⟩
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
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ ∀ z1 ∈ closedBall c1 r, ‖f (z0, 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
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑⌈b⌉₊
Tactic:
simp only [Metric.mem_closedBall] at fb ⊢
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
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, dist x c1 ≤ r → ‖f (z0, x)‖ ≤ b
⊢ ∀ (z1 : ℂ), dist z1 c1 ≤ r → ‖f (z0, 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
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, dist x c1 ≤ r → ‖f (z0, x)‖ ≤ b
⊢ ∀ (z1 : ℂ), dist z1 c1 ≤ r → ‖f (z0, z1)‖ ≤ ↑⌈b⌉₊
Tactic:
intro z1 z1r
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
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, dist x c1 ≤ r → ‖f (z0, x)‖ ≤ b
z1 : ℂ
z1r : dist z1 c1 ≤ r
⊢ ‖f (z0, 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
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, dist x c1 ≤ r → ‖f (z0, x)‖ ≤ b
z1 : ℂ
z1r : dist z1 c1 ≤ r
⊢ ‖f (z0, z1)‖ ≤ ↑⌈b⌉₊
Tactic:
exact _root_.trans (fb z1r) (Nat.le_ceil _)
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
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'
⊢ ball c0' t ⊆ closedBall c0 re
Tactic:
rw [Set.subset_def]
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
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'
⊢ ∀ x ∈ ball c0' t, x ∈ closedBall c0 re
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
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'
⊢ ∀ x ∈ ball c0' t, x ∈ closedBall c0 re
Tactic:
intro z0 z0t
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
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'
z0 : ℂ
z0t : z0 ∈ ball c0' t
⊢ z0 ∈ closedBall c0 re
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
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'
z0 : ℂ
z0t : z0 ∈ ball c0' t
⊢ z0 ∈ closedBall c0 re
Tactic:
have z0b := _root_.trans ts s's z0t
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
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'
z0 : ℂ
z0t : z0 ∈ ball c0' t
z0b : z0 ∈ S b
⊢ z0 ∈ closedBall c0 re
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
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'
z0 : ℂ
z0t : z0 ∈ ball c0' t
z0b : z0 ∈ S b
⊢ z0 ∈ closedBall c0 re
Tactic:
rw [← hS] at z0b
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
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'
z0 : ℂ
z0t : z0 ∈ ball c0' t
z0b : z0 ∈ (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) b
⊢ z0 ∈ closedBall c0 re
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
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'
z0 : ℂ
z0t : z0 ∈ ball c0' t
z0b : z0 ∈ (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) b
⊢ z0 ∈ closedBall c0 re
Tactic:
simp only [Set.setOf_and, Set.setOf_mem_eq, Set.mem_inter_iff] at z0b
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
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'
z0 : ℂ
z0t : z0 ∈ ball c0' t
z0b : z0 ∈ closedBall c0 re ∧ z0 ∈ {a | ∀ z1 ∈ closedBall c1 r, ‖f (a, z1)‖ ≤ ↑b}
⊢ z0 ∈ closedBall c0 re