map_of_continuousAt — Mathlib

English

If x ~ᵢ y and f is ContinuousAt at x and at y, then f x ~ᵢ f y.

Русский

Если x ~ᵢ y и f непрерывно в точке x и в точке y, то f(x) ~ᵢ f(y).

LaTeX

$$$(h : x \\sim_i y) \\to (ContinuousAt f x) \\to (ContinuousAt f y) \\Rightarrow f(x) \\sim_i f(y).$$$

Lean4

theorem map_of_continuousAt (h : x ~ᵢ y) (hx : ContinuousAt f x) (hy : ContinuousAt f y) : f x ~ᵢ f y :=
  h.map_of_continuousWithinAt hx.continuousWithinAt hy.continuousWithinAt (mem_univ x) (mem_univ y)

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