image_closure — Mathlib

English

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

Русский

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

LaTeX

$$$\text{ContinuousWithinAt } f\ (\overline{s}) \Rightarrow f''\overline{s} \subseteq \overline{f''s}$$$

Lean4

theorem image_closure (hf : ∀ x ∈ closure s, ContinuousWithinAt f s x) : f '' closure s ⊆ closure (f '' s) :=
  ((mapsTo_image f s).closure_of_continuousWithinAt hf).image_subset

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