closure_subset_preimage_closure_image

Mathlib.Topology.Continuous

URI: https://scilib.ai/kg/mathlib#closure_subset_preimage_closure_image

English

For a continuous map f, closure(s) is contained in the preimage of closure(f(s)).

Русский

Для непрерывного отображения f замыкание s содержится в предобразе замыкания f(s).

LaTeX

$$$\\overline{s} \\subseteq f^{-1}(\\overline{f[s]})$$$

Lean4

theorem closure_subset_preimage_closure_image (h : Continuous f) : closure s ⊆ f ⁻¹' closure (f '' s) :=
  (mapsTo_image _ _).closure h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru