continuous_left_toIocMod — Mathlib

English

If hx holds (non-equality in quotient), then toIcoMod hp a is continuous at x.

Русский

Если условие hx выполняется, то toIcoMod hp a непрерывна в x.

LaTeX

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

Lean4

theorem continuous_left_toIocMod : ContinuousWithinAt (toIocMod hp a) (Iic x) x :=
  by
  rw [(funext fun y => Eq.trans (by rw [neg_neg]) <| toIocMod_neg _ _ _ :
      toIocMod hp a = (fun x => p - x) ∘ toIcoMod hp (-a) ∘ Neg.neg)]
  exact
    (continuous_sub_left _).continuousAt.comp_continuousWithinAt <|
      (continuous_right_toIcoMod _ _ _).comp continuous_neg.continuousWithinAt fun y => neg_le_neg

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