Theorem: isClosed_𝓗 (RMT4/Spaces.lean)

State before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
⊢ IsClosed (𝓗 U)
Tactic:
refine isClosed_iff_clusterPt.2 (λ f hf => ?_)
State after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ f ∈ 𝓗 U

State before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ f ∈ 𝓗 U
Tactic:
refine @TendstoLocallyUniformlyOn.differentiableOn _ _ _ _ _ _ _ id f hf ?_ ?_ hU
State after:
case refine_1
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ TendstoLocallyUniformlyOn id f (𝓝 f ⊓ 𝓟 (𝓗 U)) U

case refine_2
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ ∀ᶠ (n : ℂ → ℂ) in 𝓝 f ⊓ 𝓟 (𝓗 U), DifferentiableOn ℂ (id n) U

State before:
case refine_1
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ TendstoLocallyUniformlyOn id f (𝓝 f ⊓ 𝓟 (𝓗 U)) U
Tactic:
simp [← tendsto_𝓒_iff hU, Tendsto]
State after:
no goals

State before:
case refine_2
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ ∀ᶠ (n : ℂ → ℂ) in 𝓝 f ⊓ 𝓟 (𝓗 U), DifferentiableOn ℂ (id n) U
Tactic:
simp [eventually_inf_principal, 𝓗]
State after:
case refine_2
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ ∀ᶠ (x : ℂ → ℂ) in 𝓝 f, x ∈ {f | DifferentiableOn ℂ f U} → DifferentiableOn ℂ x U

State before:
case refine_2
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ ∀ᶠ (x : ℂ → ℂ) in 𝓝 f, x ∈ {f | DifferentiableOn ℂ f U} → DifferentiableOn ℂ x U
Tactic:
exact eventually_of_forall (λ g => id)
State after:
no goals