closure — Mathlib

English

If a continuous map f sends s to t, then f sends closure(s) to closure(t).

Русский

Если непрерывное отображение f переводит s в t, то оно переводит замыкание s в замыкание t.

LaTeX

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

Lean4

/-- If a continuous map `f` maps `s` to `t`, then it maps `closure s` to `closure t`. -/
protected theorem closure {t : Set Y} (h : MapsTo f s t) (hc : Continuous f) : MapsTo f (closure s) (closure t) :=
  by
  simp only [MapsTo, mem_closure_iff_clusterPt]
  exact fun x hx => hx.map hc.continuousAt (tendsto_principal_principal.2 h)

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