congr_of_mem — Mathlib

English

If f is continuous within s at x and g agrees with f on all of s, then for any x in s with x in s, g is continuous within s at x provided equality holds on s.

Русский

Если f непрерывна на s в x и g совпадает с f на всем s, то при выполнении равенства на s и x∈s, g непрерывна на s в x.

LaTeX

$$$ (\forall y\in s, g(y)=f(y)) \Rightarrow (ContinuousWithinAt g s x \iff ContinuousWithinAt f s x).$$$

Lean4

theorem congr_of_mem (h : ContinuousWithinAt f s x) (h₁ : ∀ y ∈ s, g y = f y) (hx : x ∈ s) : ContinuousWithinAt g s x :=
  h.congr h₁ (h₁ x hx)

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