preimage_closure — Mathlib

English

For any subset s of Y, the preimage under e of its closure commutes with restriction: e.source ∩ e^{-1}(closure s) = e.source ∩ closure(e^{-1}(s)).

Русский

Для любого подмножества s пространства Y предобраз его замыкания через e равно e.source ∩ closure(e^{-1}(s)).

LaTeX

$$$e.source \\cap e^{-1}(\\overline{s}) = e.source \\cap \\overline{e^{-1}(s)}$$$

Lean4

theorem preimage_closure (s : Set Y) : e.source ∩ e ⁻¹' closure s = e.source ∩ closure (e ⁻¹' s) :=
  (IsImage.of_preimage_eq rfl).closure.preimage_eq

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