Theorem: tendsto_𝓒_iff (RMT4/Spaces.lean)

State before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
F : ι → 𝓒 U
f : 𝓒 U
⊢ Tendsto F l (𝓝 f) ↔ TendstoLocallyUniformlyOn F f l U
Tactic:
simp [UniformOnFun.tendsto_iff_tendstoUniformlyOn, _root_.compacts]
State after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
F : ι → 𝓒 U
f : 𝓒 U
⊢ (∀ s ⊆ U,
      IsCompact s →
        TendstoUniformlyOn (⇑(UniformOnFun.toFun {K | K ⊆ U ∧ IsCompact K}) ∘ F)
          ((UniformOnFun.toFun {K | K ⊆ U ∧ IsCompact K}) f) l s) ↔
    TendstoLocallyUniformlyOn F f l U

State before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
F : ι → 𝓒 U
f : 𝓒 U
⊢ (∀ s ⊆ U,
      IsCompact s →
        TendstoUniformlyOn (⇑(UniformOnFun.toFun {K | K ⊆ U ∧ IsCompact K}) ∘ F)
          ((UniformOnFun.toFun {K | K ⊆ U ∧ IsCompact K}) f) l s) ↔
    TendstoLocallyUniformlyOn F f l U
Tactic:
exact (tendstoLocallyUniformlyOn_iff_forall_isCompact hU).symm
State after:
no goals