restrict — Mathlib

English

If f is a function with MapsTo s t and is continuous at x, then its restriction to s is continuous at x.

Русский

Если f направлен в множество t из s и непрерывен в точке x, то ограничение функции на s непрерывно в x.

LaTeX

$$$\text{MapsTo}(f, s, t) \to \text{ContinuousAt}(f, x) \Rightarrow \text{ContinuousAt}(f|_s, x).$$$

Lean4

theorem restrict {f : X → Y} {s : Set X} {t : Set Y} (h1 : MapsTo f s t) {x : s} (h2 : ContinuousAt f x) :
    ContinuousAt (h1.restrict f s t) x :=
  (h2.comp continuousAt_subtype_val).codRestrict _

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