case intro.intro
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
δ : ℝ
hδ : 0 < δ
hKδ : cthickening δ K ⊆ U
⊢ ∃ δ, δ > 0 ∧ cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∃ δ, δ > 0 ∧ cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
obtain ⟨δ, hδ, hKδ⟩ := hK.exists_cthickening_subset_open hU hKU
no goals
case intro.intro
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
δ : ℝ
hδ : 0 < δ
hKδ : cthickening δ K ⊆ U
⊢ ∃ δ, δ > 0 ∧ cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
exact ⟨δ, hδ, hKδ, tendstoUniformlyOn_deriv_of_cthickening_subset hf hF hδ hK hU hKδ⟩