continuousWithinAt_dslope_of_ne — Mathlib

English

For b ≠ a, dslope f a within s at b is equivalent to f within s at b (alternative formulation).

Русский

Для b ≠ a dslope f a в пределах s в точке b эквивалентна f в пределах s в точке b.

LaTeX

$$$\text{ContinuousWithinAt}( dslope\ f\ a, s, b) \iff \text{ContinuousWithinAt}( f, s, b) \quad (b \neq a)$$$

Lean4

theorem continuousWithinAt_dslope_of_ne (h : b ≠ a) : ContinuousWithinAt (dslope f a) s b ↔ ContinuousWithinAt f s b :=
  by
  refine ⟨ContinuousWithinAt.of_dslope, fun hc => ?_⟩
  classical
  simp only [dslope, continuousWithinAt_update_of_ne h]
  exact
    ((continuousWithinAt_id.sub continuousWithinAt_const).inv₀ (sub_ne_zero.2 h)).smul (hc.sub continuousWithinAt_const)

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