continuousAt_toIcoMod — Mathlib

English

For non-equal quotient elements, continuousAt of toIcoMod holds as a consequence of earlier lemmas.

Русский

Для элементов, не равных по делению, непрерывность toIcoMod следует из предыдущих лемм.

LaTeX

$$continuousAt_toIcoMod hp a (hx) : ContinuousAt (toIcoMod hp a) x$$

Lean4

theorem continuousAt_toIcoMod (hx : (x : 𝕜 ⧸ zmultiples p) ≠ a) : ContinuousAt (toIcoMod hp a) x :=
  let h := toIcoMod_eventuallyEq_toIocMod hp a hx
  continuousAt_iff_continuous_left_right.2 <|
    ⟨(continuous_left_toIocMod hp a x).congr_of_eventuallyEq (h.filter_mono nhdsWithin_le_nhds) h.eq_of_nhds,
      continuous_right_toIcoMod hp a x⟩

Похожие утверждения