map_of_continuousWithinAt — Mathlib

English

If x ~ᵢ y and f is ContinuousWithinAt on s at x and on t at y with x∈t and y∈s, then f x ~ᵢ f y.

Русский

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

LaTeX

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

Lean4

theorem map_of_continuousWithinAt {s t : Set X} (h : x ~ᵢ y) (hfx : ContinuousWithinAt f s x)
    (hfy : ContinuousWithinAt f t y) (hx : x ∈ t) (hy : y ∈ s) : f x ~ᵢ f y :=
  (h.specializes.map_of_continuousWithinAt hfy hx).antisymm (h.specializes'.map_of_continuousWithinAt hfx hy)

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