congr — Mathlib

English

If f is continuous on s at x and g agrees with f on s, and g(x)=f(x), then g is continuous on s at x.

Русский

Если f непрерывна на s в x, и g совпадает с f на s, а также g(x)=f(x), то g непрерывна на s в x.

LaTeX

$$$ \text{If } f\downarrow_s x \text{ and } (\forall y\in s, g(y)=f(y)) \text{ and } g(x)=f(x), \text{ then } g\downarrow_s x.$$$

Lean4

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

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