map_closure — Mathlib

English

Image of the closure equals the closure of the image.

Русский

Образ замыкания равен замыканию образа.

LaTeX

$$$\\mathrm{map}\\ f(\\mathrm{closure}(s)) = \\mathrm{closure}(f''s)$$$

Lean4

theorem map_closure (f : M →[L] N) (s : Set M) : (closure L s).map f = closure L (f '' s) :=
  Eq.symm <|
    closure_eq_of_le (Set.image_mono subset_closure) <|
      map_le_iff_le_comap.2 <| closure_le.2 fun x hx => subset_closure ⟨x, hx, rfl⟩

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