image_closure — Mathlib

English

If f is continuous on closure s, then the image of closure s is contained in the closure of the image of s.

Русский

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

LaTeX

$$$\text{ContinuousOn } f\ (\overline{s}) \to f''\overline{s} \subseteq \overline{f''s}$$$

Lean4

theorem image_closure (hf : ContinuousOn f (closure s)) : f '' closure s ⊆ closure (f '' s) :=
  ContinuousWithinAt.image_closure fun x hx => (hf x hx).mono subset_closure

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