continuousWithinAt_Icc_iff_Iic — Mathlib

English

For a < b, a function f is continuous at b on the closed interval Icc(a,b) if and only if it is continuous at b on the left-closed ray Iic(b).

Русский

Для a < b функция f непрерывна в точке b на замкнутом интервале Icc(a,b) тогда и только тогда, когда она непрерывна слева на луче Iic(b).

LaTeX

$$$ a < b \rightarrow (ContinuousWithinAt f (Icc a b) b \leftrightarrow ContinuousWithinAt f (Iic b) b) $$$

Lean4

@[simp]
theorem continuousWithinAt_Icc_iff_Iic (h : a < b) :
    ContinuousWithinAt f (Icc a b) b ↔ ContinuousWithinAt f (Iic b) b := by
  simp only [ContinuousWithinAt, nhdsWithin_Icc_eq_nhdsLE h]

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