image_closure — Mathlib

English

The image under a continuous algebra equivalence commutes with taking closures: e''closure S = closure (e''S).

Русский

Образ при непрерывном алгебровом эквививаленте коммутирует со взятием замыкания: e'' closure S = closure (e''S).

LaTeX

$$$ e''\overline{S} = \overline{e''S} $$$

Lean4

theorem image_closure (e : A ≃A[R] B) (S : Set A) : e '' closure S = closure (e '' S) :=
  e.toHomeomorph.image_closure S

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