continuousWithinAt_Ioc_iff_Iic — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem continuousWithinAt_Ioc_iff_Iic (h : a < b) :
    ContinuousWithinAt f (Ioc a b) b ↔ ContinuousWithinAt f (Iic b) b := by
  simp only [ContinuousWithinAt, nhdsWithin_Ioc_eq_nhdsLE h]

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