Theorem: TendstoUniformlyOn.inv_of_compact (RMT4/hurwitz.lean)

State before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hf : ContinuousOn f K
hK : IsCompact K
hfz : ∀ x ∈ K, f x ≠ 0
⊢ TendstoUniformlyOn F⁻¹ f⁻¹ p K
Tactic:
apply hF.inv
State after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hf : ContinuousOn f K
hK : IsCompact K
hfz : ∀ x ∈ K, f x ≠ 0
⊢ 𝓟 (f '' K) ⊓ 𝓝 0 = ⊥

State before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hf : ContinuousOn f K
hK : IsCompact K
hfz : ∀ x ∈ K, f x ≠ 0
⊢ 𝓟 (f '' K) ⊓ 𝓝 0 = ⊥
Tactic:
rw [inf_comm, inf_principal_eq_bot]
State after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hf : ContinuousOn f K
hK : IsCompact K
hfz : ∀ x ∈ K, f x ≠ 0
⊢ (f '' K)ᶜ ∈ 𝓝 0

State before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hf : ContinuousOn f K
hK : IsCompact K
hfz : ∀ x ∈ K, f x ≠ 0
⊢ (f '' K)ᶜ ∈ 𝓝 0
Tactic:
exact (hK.image_of_continuousOn hf).isClosed.compl_mem_nhds (λ ⟨z, h1, h2⟩ => hfz z h1 h2)
State after:
no goals