English
Let p > 0. For any a ∈ 𝕜 and x ∈ 𝕜 with the coset of x in 𝕜 modulo zmultiples p distinct from a, the map toIocMod hp a is continuous at x.
Русский
Пусть p > 0. Для любых a ∈ 𝕜 и x ∈ 𝕜, если косет x по модулю zmultiples p не равен a, то функция toIocMod hp a непрерывна в точке x.
LaTeX
$$$0 < p \Rightarrow \forall a \in 𝕜, \forall x \in 𝕜, (x : 𝕜 \;⧸\; zmultiples\,p) \neq a \Rightarrow \operatorname{ContinuousAt} (toIocMod hp a) x$$$
Lean4
theorem continuousAt_toIocMod (hx : (x : 𝕜 ⧸ zmultiples p) ≠ a) : ContinuousAt (toIocMod hp a) x :=
let h := toIcoMod_eventuallyEq_toIocMod hp a hx
continuousAt_iff_continuous_left_right.2 <|
⟨continuous_left_toIocMod hp a x,
(continuous_right_toIcoMod hp a x).congr_of_eventuallyEq (h.symm.filter_mono nhdsWithin_le_nhds)
h.symm.eq_of_nhds⟩
