closure_of_continuousWithinAt — Mathlib

English

If f maps s into t and is continuous within s near every point of closure s, then maps closure s into closure t.

Русский

Если f переводит s в t и непрерывна в окрестностях каждой точки closure s, то closure s отображается в closure t.

LaTeX

$$$\text{MapsTo } f\ s\ t \to (\forall x \in \overline{s}, \text{ContinuousWithinAt } f\ s\ x) \to \text{MapsTo } f\ \overline{s}\ \overline{t}$$$

Lean4

theorem closure_of_continuousWithinAt {t : Set β} (h : MapsTo f s t) (hc : ∀ x ∈ closure s, ContinuousWithinAt f s x) :
    MapsTo f (closure s) (closure t) := fun x hx => (hc x hx).mem_closure hx h

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