closure_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- If a continuous map `f` maps `s` to a closed set `t`, then it maps `closure s` to `t`. -/
theorem closure_left {t : Set Y} (h : MapsTo f s t) (hc : Continuous f) (ht : IsClosed t) : MapsTo f (closure s) t :=
  ht.closure_eq ▸ h.closure hc

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