closure_of_continuousOn — Mathlib

English

If f maps s into t and is continuous on closure s, then f maps closure s into closure t.

Русский

Если образ s принадлежит t и f непрерывна на closure s, то f(closure s) ⊆ closure t.

LaTeX

$$$\text{MapsTo } f\ s\ t \to \text{ContinuousOn } f\ (\overline{s}) \to \text{MapsTo } f\ \overline{s}\ \overline{t}$$$

Lean4

theorem closure_of_continuousOn {t : Set β} (h : MapsTo f s t) (hc : ContinuousOn f (closure s)) :
    MapsTo f (closure s) (closure t) :=
  h.closure_of_continuousWithinAt fun x hx => (hc x hx).mono subset_closure

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