continuousWithinAt_Ioc_iff_Ioi — Mathlib

English

For a < b, a function f is continuous at a from inside Ioc(a,b) if and only if it is continuous at a from inside Ioi(a).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem continuousWithinAt_Ioc_iff_Ioi (h : a < b) :
    ContinuousWithinAt f (Ioc a b) a ↔ ContinuousWithinAt f (Ioi a) a := by
  simp only [ContinuousWithinAt, nhdsWithin_Ioc_eq_nhdsGT h]

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