map_mem_closure — Mathlib

English

If f is continuous, x ∈ closure(s), and MapsTo f s t, then f(x) ∈ closure(t).

Русский

Если f непрерывна, x лежит в замыкании s, и MapsTo(f,s,t), то f(x) лежит в замыкании t.

LaTeX

$$$\\text{Continuous}(f) \\land x \\in \\overline{s} \\land \\text{MapsTo}(f,s,t) \\Rightarrow f(x) \\in \\overline{t}$$$

Lean4

theorem map_mem_closure {t : Set Y} (hf : Continuous f) (hx : x ∈ closure s) (ht : MapsTo f s t) : f x ∈ closure t :=
  ht.closure hf hx

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