closure_eq_preimage_closure_image

Mathlib.Topology.Maps.Basic

URI: https://scilib.ai/kg/mathlib#Topology.IsEmbedding.closure_eq_preimage_closure_image

← MathLib Explorer

English

For an embedding f and any subset s ⊆ X, closure(s) = f^{-1}(closure(f''s)).

Русский

При вложении f и любом подмножестве s ⊆ X верно closure(s) = f^{-1}(closure(f''s)).

LaTeX

$$$\mathrm{closure}(s) = f^{-1}\left(\mathrm{closure}(f''s)\right)$$$

Lean4

theorem closure_eq_preimage_closure_image (hf : IsEmbedding f) (s : Set X) : closure s = f ⁻¹' closure (f '' s) :=
  hf.1.closure_eq_preimage_closure_image s

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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