Theorem: TendstoUniformlyOn.inv (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 : ℝ
hF : TendstoUniformlyOn F f p s
hf : 𝓟 (f '' s) ⊓ 𝓝 0 = ⊥
⊢ TendstoUniformlyOn F⁻¹ f⁻¹ p s
Tactic:
have : 𝓝ᵘ (f '' s) ⊓ 𝓝 0 = ⊥ := by
  rw [inf_comm] at hf ⊢
  exact UniformSpace.nhds_inf_uniform_nhds_eq_bot hf
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 : ℝ
hF : TendstoUniformlyOn F f p s
hf : 𝓟 (f '' s) ⊓ 𝓝 0 = ⊥
this : 𝓝ᵘ (f '' s) ⊓ 𝓝 0 = ⊥
⊢ TendstoUniformlyOn F⁻¹ f⁻¹ p s

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 : ℝ
hF : TendstoUniformlyOn F f p s
hf : 𝓟 (f '' s) ⊓ 𝓝 0 = ⊥
this : 𝓝ᵘ (f '' s) ⊓ 𝓝 0 = ⊥
⊢ TendstoUniformlyOn F⁻¹ f⁻¹ p s
Tactic:
have h1 := lemma1 hF
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 : ℝ
hF : TendstoUniformlyOn F f p s
hf : 𝓟 (f '' s) ⊓ 𝓝 0 = ⊥
this : 𝓝ᵘ (f '' s) ⊓ 𝓝 0 = ⊥
h1 : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓟 (f '' s) ×ˢ 𝓝ᵘ (f '' s))
⊢ TendstoUniformlyOn F⁻¹ f⁻¹ p s

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 : ℝ
hF : TendstoUniformlyOn F f p s
hf : 𝓟 (f '' s) ⊓ 𝓝 0 = ⊥
this : 𝓝ᵘ (f '' s) ⊓ 𝓝 0 = ⊥
h1 : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓟 (f '' s) ×ˢ 𝓝ᵘ (f '' s))
⊢ TendstoUniformlyOn F⁻¹ f⁻¹ p s
Tactic:
rw [tendstoUniformlyOn_iff_tendsto] at hF ⊢
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 : ℝ
hF : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 𝕜)
hf : 𝓟 (f '' s) ⊓ 𝓝 0 = ⊥
this : 𝓝ᵘ (f '' s) ⊓ 𝓝 0 = ⊥
h1 : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓟 (f '' s) ×ˢ 𝓝ᵘ (f '' s))
⊢ Tendsto (fun q => (f⁻¹ q.2, F⁻¹ q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 𝕜)

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 : ℝ
hF : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 𝕜)
hf : 𝓟 (f '' s) ⊓ 𝓝 0 = ⊥
this : 𝓝ᵘ (f '' s) ⊓ 𝓝 0 = ⊥
h1 : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓟 (f '' s) ×ˢ 𝓝ᵘ (f '' s))
⊢ Tendsto (fun q => (f⁻¹ q.2, F⁻¹ q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 𝕜)
Tactic:
refine (Filter.map_mono (le_inf hF h1)).trans (titi hf this)
State after:
no goals

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 : ℝ
hF : TendstoUniformlyOn F f p s
hf : 𝓟 (f '' s) ⊓ 𝓝 0 = ⊥
⊢ 𝓝ᵘ (f '' s) ⊓ 𝓝 0 = ⊥
Tactic:
rw [inf_comm] at hf ⊢
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 : ℝ
hF : TendstoUniformlyOn F f p s
hf : 𝓝 0 ⊓ 𝓟 (f '' s) = ⊥
⊢ 𝓝 0 ⊓ 𝓝ᵘ (f '' s) = ⊥

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 : ℝ
hF : TendstoUniformlyOn F f p s
hf : 𝓝 0 ⊓ 𝓟 (f '' s) = ⊥
⊢ 𝓝 0 ⊓ 𝓝ᵘ (f '' s) = ⊥
Tactic:
exact UniformSpace.nhds_inf_uniform_nhds_eq_bot hf
State after:
no goals