Theorem: uniform_ContinuousOn_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 : ℝ
s : Set 𝕜
hs : 𝓟 s ⊓ 𝓝 0 = ⊥
⊢ UniformContinuousOn Inv.inv s
Tactic:
simpa only [UniformContinuousOn, Tendsto, ← prod_principal_principal] using titi hs hs
State after:
no goals