continuousWithinAt_congr_of_mem — Mathlib

English

Let f,g: X→Y, s⊆X, x∈s. If f and g are EventuallyEq with respect to nhdsWithin x s, then ContinuousWithinAt f s x ⇔ ContinuousWithinAt g s x.

Русский

Пусть f,g: X→Y, s⊆X, x∈s. Если f и g эквивалентны почти всюду в 𝓝[x]∩s, то непрерывность f на s в x эквивалентна непрерывности g на s в x.

LaTeX

$$$ (f =^{\mathcal{N}[s] x} g) \Rightarrow (ContinuousWithinAt f s x \iff ContinuousWithinAt g s x).$$$

Lean4

theorem continuousWithinAt_congr_of_mem (h₁ : ∀ y ∈ s, g y = f y) (hx : x ∈ s) :
    ContinuousWithinAt g s x ↔ ContinuousWithinAt f s x :=
  continuousWithinAt_congr h₁ (h₁ x hx)

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