ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
⊢ Cauchy (map (fun n => f n x) l)
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
⊢ Cauchy (map (fun n => f n x) l)
have : NeBot l := (cauchy_map_iff.1 hfg).1
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
⊢ Cauchy (map (fun n => f n x) l)
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
⊢ Cauchy (map (fun n => f n x) l)
let t := { y | y ∈ s ∧ Cauchy (map (fun n => f n y) l) }
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
H : s ⊆ t
⊢ Cauchy (map (fun n => f n x) l)

case H
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
⊢ s ⊆ t
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
⊢ Cauchy (map (fun n => f n x) l)
suffices H : s ⊆ t
case H
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
⊢ s ⊆ t
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
H : s ⊆ t
⊢ Cauchy (map (fun n => f n x) l)

case H
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
⊢ s ⊆ t
exact (H hx).2
case H
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
⊢ s ⊆ t
case H
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
⊢ s ⊆ t
have A : ∀ x ε, x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t := fun x ε xt hx y hy =>
  ⟨hx hy,
    (uniformCauchySeqOn_ball_of_fderiv (hf'.mono hx) (fun n y hy => hf n y (hx hy))
          xt.2).cauchy_map
      hy⟩
case H
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
⊢ s ⊆ t
case H
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
⊢ s ⊆ t
have open_t : IsOpen t := by
  rw [Metric.isOpen_iff]
  intro x hx
  rcases Metric.isOpen_iff.1 hs x hx.1 with ⟨ε, εpos, hε⟩
  exact ⟨ε, εpos, A x ε hx hε⟩
case H
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
⊢ s ⊆ t
case H
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
⊢ s ⊆ t
have st_nonempty : (s ∩ t).Nonempty := ⟨x₀, hx₀, ⟨hx₀, hfg⟩⟩
case H
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
H : closure t ∩ s ⊆ t
⊢ s ⊆ t

case H
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
⊢ closure t ∩ s ⊆ t
case H
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
⊢ s ⊆ t
suffices H : closure t ∩ s ⊆ t
case H
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
⊢ closure t ∩ s ⊆ t
case H
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
H : closure t ∩ s ⊆ t
⊢ s ⊆ t

case H
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
⊢ closure t ∩ s ⊆ t
exact h's.subset_of_closure_inter_subset open_t st_nonempty H
case H.intro
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝¹ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx : x✝ ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
x : E
xt : x ∈ closure t
xs : x ∈ s
⊢ x ∈ t
case H
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
⊢ closure t ∩ s ⊆ t
rintro x ⟨xt, xs⟩
case H.intro.intro.intro
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝¹ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx : x✝ ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
x : E
xt : x ∈ closure t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
⊢ x ∈ t
case H.intro
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝¹ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx : x✝ ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
x : E
xt : x ∈ closure t
xs : x ∈ s
⊢ x ∈ t
obtain ⟨ε, εpos, hε⟩ : ∃ (ε : ℝ), ε > 0 ∧ Metric.ball x ε ⊆ s := Metric.isOpen_iff.1 hs x xs
case H.intro.intro.intro.intro.intro
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝¹ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx : x✝ ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
x : E
xt : x ∈ closure t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
⊢ x ∈ t
case H.intro.intro.intro
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝¹ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx : x✝ ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
x : E
xt : x ∈ closure t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
⊢ x ∈ t
obtain ⟨y, yt, hxy⟩ : ∃ (y : E), y ∈ t ∧ dist x y < ε / 2 :=
  Metric.mem_closure_iff.1 xt _ (half_pos εpos)
case H.intro.intro.intro.intro.intro
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝¹ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx : x✝ ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
x : E
xt : x ∈ closure t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
B : Metric.ball y (ε / 2) ⊆ Metric.ball x ε
⊢ x ∈ t
case H.intro.intro.intro.intro.intro
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝¹ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx : x✝ ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
x : E
xt : x ∈ closure t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
⊢ x ∈ t
have B : Metric.ball y (ε / 2) ⊆ Metric.ball x ε := by
  apply Metric.ball_subset_ball'; rw [dist_comm]; linarith
no goals
case H.intro.intro.intro.intro.intro
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝¹ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx : x✝ ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
x : E
xt : x ∈ closure t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
B : Metric.ball y (ε / 2) ⊆ Metric.ball x ε
⊢ x ∈ t
exact A y (ε / 2) yt (B.trans hε) (Metric.mem_ball.2 hxy)
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
⊢ ∀ (x : E), x ∈ t → ∃ ε, ε > 0 ∧ Metric.ball x ε ⊆ t
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
⊢ IsOpen t
rw [Metric.isOpen_iff]
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝¹ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx✝ : x✝ ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
x : E
hx : x ∈ t
⊢ ∃ ε, ε > 0 ∧ Metric.ball x ε ⊆ t
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
⊢ ∀ (x : E), x ∈ t → ∃ ε, ε > 0 ∧ Metric.ball x ε ⊆ t
intro x hx
case intro.intro
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝¹ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx✝ : x✝ ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
x : E
hx : x ∈ t
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
⊢ ∃ ε, ε > 0 ∧ Metric.ball x ε ⊆ t
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝¹ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx✝ : x✝ ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
x : E
hx : x ∈ t
⊢ ∃ ε, ε > 0 ∧ Metric.ball x ε ⊆ t
rcases Metric.isOpen_iff.1 hs x hx.1 with ⟨ε, εpos, hε⟩
no goals
case intro.intro
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝¹ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx✝ : x✝ ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
x : E
hx : x ∈ t
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
⊢ ∃ ε, ε > 0 ∧ Metric.ball x ε ⊆ t
exact ⟨ε, εpos, A x ε hx hε⟩
case h
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝¹ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx : x✝ ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
x : E
xt : x ∈ closure t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
⊢ ε / 2 + dist y x ≤ ε
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝¹ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx : x✝ ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
x : E
xt : x ∈ closure t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
⊢ Metric.ball y (ε / 2) ⊆ Metric.ball x ε
apply Metric.ball_subset_ball'
case h
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝¹ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx : x✝ ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
x : E
xt : x ∈ closure t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
⊢ ε / 2 + dist x y ≤ ε
case h
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝¹ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx : x✝ ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
x : E
xt : x ∈ closure t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
⊢ ε / 2 + dist y x ≤ ε
rw [dist_comm]
no goals
case h
ι : Type u_3
l : Filter ι
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_4
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x✝¹ : E
s : Set E
hs : IsOpen s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι) (y : E), y ∈ s → HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx : x✝ ∈ s
hfg : Cauchy (map (fun n => f n x₀) l)
this : NeBot l
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n => f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen t
st_nonempty : Set.Nonempty (s ∩ t)
x : E
xt : x ∈ closure t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
⊢ ε / 2 + dist x y ≤ ε
linarith