continuousAt_equivIoc — Mathlib

English

If x ≠ a, the map equivIco p a is continuous at x.

Русский

Если x ≠ a, отображение equivIco p a непрерывно в точке x.

LaTeX

$$$$ \forall x \neq a, \operatorname{ContinuousAt} (equivIco\ p\ a) x $$$$

Lean4

theorem continuousAt_equivIoc (hx : x ≠ a) : ContinuousAt (equivIoc p a) x :=
  by
  induction x using QuotientAddGroup.induction_on
  rw [ContinuousAt, Filter.Tendsto, QuotientAddGroup.nhds_eq, Filter.map_map]
  exact (continuousAt_toIocMod hp.out a hx).codRestrict _

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