continuousWithinAt_Ioo_iff_Iio — Mathlib

English

For a < b, a function is continuous at b from inside Ioo(a,b) if and only if it is continuous at b from inside Iio(b).

Русский

Для a < b непрерывность в точке b изнутри Ioo(a,b) эквивалентна непрерывности изнутри Iio(b).

LaTeX

$$$(a

Lean4

@[simp]
theorem continuousWithinAt_Ioo_iff_Iio (h : a < b) :
    ContinuousWithinAt f (Ioo a b) b ↔ ContinuousWithinAt f (Iio b) b := by
  simp only [ContinuousWithinAt, nhdsWithin_Ioo_eq_nhdsLT h]

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