English
Let K be a field with a compatible uniform structure. In the completion hat K, the inverse map extends continuously at every nonzero point: for every x in hat K with x ≠ 0, the map that sends t to t^{-1} is continuous at x.
Русский
Пусть K — поле с подходящей униформной структурой. В дополнении hat K обратная карта продолжена непрерывно в любой ненулевой точке: для каждого x ∈ hat K с x ≠ 0 отображение t ↦ t^{-1} непрерывно в точке x.
LaTeX
$$$\mathrm{ContinuousAt}(\hatInv, x)$$$
Lean4
@[fun_prop]
theorem continuous_hatInv [CompletableTopField K] {x : hat K} (h : x ≠ 0) : ContinuousAt hatInv x :=
by
refine isDenseInducing_coe.continuousAt_extend ?_
apply mem_of_superset (compl_singleton_mem_nhds h)
intro y y_ne
rw [mem_compl_singleton_iff] at y_ne
apply CompleteSpace.complete
have : (fun (x : K) => (↑x⁻¹ : hat K)) = ((fun (y : K) => (↑y : hat K)) ∘ (fun (x : K) => (x⁻¹ : K))) :=
by
unfold Function.comp
simp
rw [this, ← Filter.map_map]
apply Cauchy.map _ (Completion.uniformContinuous_coe K)
apply CompletableTopField.nice
· haveI := isDenseInducing_coe.comap_nhds_neBot y
apply cauchy_nhds.comap
rw [Completion.comap_coe_eq_uniformity]
· have eq_bot : 𝓝 (0 : hat K) ⊓ 𝓝 y = ⊥ := by
by_contra h
exact y_ne (eq_of_nhds_neBot <| neBot_iff.mpr h).symm
rw [isDenseInducing_coe.nhds_eq_comap (0 : K), ← Filter.comap_inf]
norm_cast
rw [eq_bot]
exact comap_bot
