congr — Mathlib

English

If g equals f pointwise, then continuity of f implies continuity of g.

Русский

Если функция g совпадает с f по точкам, то непрерывность f приводит к непрерывности g.

LaTeX

$$$\forall g, (h : \mathrm{Continuous}(f)) \rightarrow (\forall x, f(x) = g(x)) \rightarrow \mathrm{Continuous}(g).$$$

Lean4

theorem congr {g : X → Y} (h : Continuous f) (h' : ∀ x, f x = g x) : Continuous g :=
  continuous_congr h' |>.mp h

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