restrict — Mathlib

English

If the images of a subset s under f land in t and f is continuous on X, then the restricted map f|_s: s → t is continuous.

Русский

Пусть f: X → Y непрерывно на X, и f(s) ⊆ t. Тогда ограничение f на s: s → t непрерывно.

LaTeX

$$$\\forall f:X\\to Y,\\; \\forall s,t,\\; (f(s)\\subseteq t) \\Rightarrow \\text{Continuous}\\left(f\\big|_{s}\\right).$$$

Lean4

@[continuity, fun_prop]
theorem restrict {f : X → Y} {s : Set X} {t : Set Y} (h1 : MapsTo f s t) (h2 : Continuous f) :
    Continuous (h1.restrict f s t) :=
  (h2.comp continuous_subtype_val).codRestrict _

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