map_of_continuousOn — Mathlib

English

If x ~ᵢ y and f is ContinuousOn on s, and x,y ∈ s, then f x ~ᵢ f y.

Русский

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

LaTeX

$$$(h : x \\sim_i y) \\to (ContinuousOn f s) \\to x \\in s \\to y \\in s \\Rightarrow f(x) \\sim_i f(y).$$$

Lean4

theorem map_of_continuousOn {s : Set X} (h : x ~ᵢ y) (hf : ContinuousOn f s) (hx : x ∈ s) (hy : y ∈ s) : f x ~ᵢ f y :=
  h.map_of_continuousWithinAt (hf.continuousWithinAt hx) (hf.continuousWithinAt hy) hx hy

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