continuousWithinAt_Iio_iff_Iic — Mathlib

English

Dual statement to above: continuity from the left of a equals continuity from the right for Iio a and Iic a.

Русский

Дуальная версия: непрерывность слева на Iio a равна непрерывности справа на Iic a.

LaTeX

$$theorem continuousWithinAt_Iio_iff_Iic {a : α} {f : α → β} : ContinuousWithinAt f (Iio a) a ↔ ContinuousWithinAt f (Iic a) a$$

Lean4

theorem continuousWithinAt_Iio_iff_Iic {a : α} {f : α → β} :
    ContinuousWithinAt f (Iio a) a ↔ ContinuousWithinAt f (Iic a) a :=
  continuousWithinAt_Ioi_iff_Ici (α := αᵒᵈ)

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