internlm/Lean-Github huggingface dataset:
Theorem: ContinuousOn.isClosed_le
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✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
⊢ IsClosed {x | x ∈ s ∧ f x ≤ g x}
Tactic:
rw [Set.setOf_and]
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✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
⊢ IsClosed ({a | a ∈ s} ∩ {a | f a ≤ g a})
Theorem: ContinuousOn.isClosed_le
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✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
⊢ IsClosed ({a | a ∈ s} ∩ {a | f a ≤ g a})
Tactic:
simp only [Set.setOf_mem_eq]
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✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
⊢ IsClosed (s ∩ {a | f a ≤ g a})
Theorem: ContinuousOn.isClosed_le
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✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
⊢ IsClosed (s ∩ {a | f a ≤ g a})
Tactic:
set t := {p : B × B | p.fst ≤ p.snd}
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✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
⊢ IsClosed (s ∩ {a | f a ≤ g a})
Theorem: ContinuousOn.isClosed_le
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✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
⊢ IsClosed (s ∩ {a | f a ≤ g a})
Tactic:
set fg := fun x ↦ (f x, g x)
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✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
⊢ IsClosed (s ∩ {a | f a ≤ g a})
Theorem: ContinuousOn.isClosed_le
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✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
⊢ IsClosed (s ∩ {a | f a ≤ g a})
Tactic:
have e : {x | f x ≤ g x} = fg ⁻¹' t := by
  apply Set.ext; intro x; simp only [Set.preimage_setOf_eq, t]
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✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
e : {x | f x ≤ g x} = fg ⁻¹' t
⊢ IsClosed (s ∩ {a | f a ≤ g a})
Theorem: ContinuousOn.isClosed_le
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✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
e : {x | f x ≤ g x} = fg ⁻¹' t
⊢ IsClosed (s ∩ {a | f a ≤ g a})
Tactic:
rw [e]
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✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
e : {x | f x ≤ g x} = fg ⁻¹' t
⊢ IsClosed (s ∩ fg ⁻¹' t)
Theorem: ContinuousOn.isClosed_le
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✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
e : {x | f x ≤ g x} = fg ⁻¹' t
⊢ IsClosed (s ∩ fg ⁻¹' t)
Tactic:
exact ContinuousOn.preimage_isClosed_of_isClosed (ContinuousOn.prod fc gc) sc
  OrderClosedTopology.isClosed_le'
Proof state after:
no goals
Theorem: ContinuousOn.isClosed_le
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✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
⊢ {x | f x ≤ g x} = fg ⁻¹' t
Tactic:
apply Set.ext
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 : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
⊢ ∀ (x : A), x ∈ {x | f x ≤ g x} ↔ x ∈ fg ⁻¹' t
Theorem: ContinuousOn.isClosed_le
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 : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
⊢ ∀ (x : A), x ∈ {x | f x ≤ g x} ↔ x ∈ fg ⁻¹' t
Tactic:
intro x
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 : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
x : A
⊢ x ∈ {x | f x ≤ g x} ↔ x ∈ fg ⁻¹' t
Theorem: ContinuousOn.isClosed_le
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 : ℝ
A B : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : Preorder B
inst✝ : OrderClosedTopology B
s : Set A
f g : A → B
sc : IsClosed s
fc : ContinuousOn f s
gc : ContinuousOn g s
t : Set (B × B) := {p | p.1 ≤ p.2}
fg : A → B × B := fun x => (f x, g x)
x : A
⊢ x ∈ {x | f x ≤ g x} ↔ x ∈ fg ⁻¹' t
Tactic:
simp only [Set.preimage_setOf_eq, t]
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
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
set re := min r e
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
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
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
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
have esub : closedBall c0 re ⊆ closedBall c0 r :=
  Metric.closedBall_subset_closedBall (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 (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
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
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
generalize hS : (fun b : ℕ ↦
  {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1, z1 ∈ closedBall c1 r → ‖f (z0, z1)‖ ≤ b}) = S
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
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
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)
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
have hU : (interior (⋃ b, S b)).Nonempty := by
  refine Set.nonempty_of_mem
      (mem_interior.mpr ⟨ball c0 re, ?_, Metric.isOpen_ball, Metric.mem_ball_self (lt_min rp ep)⟩)
  rw [Set.subset_def]; intro z0 z0s; rw [Set.mem_iUnion]
  have z0s' := esub (mem_open_closed z0s)
  rcases (isCompact_closedBall _ _).bddAbove_image (h.on1 z0s').continuousOn.norm with ⟨b, fb⟩
  simp only [mem_upperBounds, Set.forall_mem_image] at fb
  use Nat.ceil b; rw [← hS]; simp only [Set.mem_setOf]
  refine ⟨mem_open_closed z0s, ?_⟩
  simp only [Metric.mem_closedBall] at fb ⊢; intro z1 z1r
  exact _root_.trans (fb z1r) (Nat.le_ceil _)
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
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
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
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
rcases NonemptyInterior.nonempty_interior_of_iUnion_of_closed hc hU with ⟨b, bi⟩
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)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
bi : (interior (S b)).Nonempty
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
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)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
bi : (interior (S b)).Nonempty
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
rcases bi with ⟨c0', c0's⟩
Proof state after:
case 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)
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Theorem: on_subdisk
Proof state before:
case 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)
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
use c0'
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)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
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)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
rcases mem_interior.mp c0's with ⟨s', s's, so, c0s'⟩
Proof state after:
case h.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 > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Theorem: on_subdisk
Proof state before:
case h.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 > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
rcases Metric.isOpen_iff.mp so c0' c0s' with ⟨t, tp, ts⟩
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'
⊢ ∃ 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'
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
have tr : ball c0' t ⊆ closedBall c0 re := by
  rw [Set.subset_def]; intro z0 z0t
  have z0b := _root_.trans ts s's z0t
  rw [← hS] at z0b; simp only [Set.setOf_and, Set.setOf_mem_eq, Set.mem_inter_iff] at z0b
  exact z0b.left
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
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)