continuousWithinAt_Ioi_iff_Ici — Mathlib

English

For a and f, continuity from the right is equivalent to continuity from the left at a for Ioi a and Ici a respectively.

Русский

Для любого a и f эквивалентны непрерывности слева и справа на Ioi a и Ici a.

LaTeX

$$theorem continuousWithinAt_Ioi_iff_Ici {a : α} {f : α → β} : ContinuousWithinAt f (Ioi a) a ↔ ContinuousWithinAt f (Ici a) a$$

Lean4

theorem continuousWithinAt_Ioi_iff_Ici {a : α} {f : α → β} :
    ContinuousWithinAt f (Ioi a) a ↔ ContinuousWithinAt f (Ici a) a := by
  simp only [← Ici_diff_left, continuousWithinAt_diff_self]

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