continuousWithinAt_Ioo_iff_Ioi — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem continuousWithinAt_Ioo_iff_Ioi (h : a < b) :
    ContinuousWithinAt f (Ioo a b) a ↔ ContinuousWithinAt f (Ioi a) a := by
  simp only [ContinuousWithinAt, nhdsWithin_Ioo_eq_nhdsGT h]

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