closure_eq_preimage_closure_image

Mathlib.Topology.Maps.Basic

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

← MathLib Explorer

English

For hf IsInducing, closure s = f⁻¹' closure (f '' s).

Русский

Для индуциирующего f выполняется closure s = f⁻¹' closure (f '' s).

LaTeX

$$$\operatorname{closure}(s) = f^{-1}(\operatorname{closure}(f(s))).$$$

Lean4

theorem closure_eq_preimage_closure_image (hf : IsInducing f) (s : Set X) : closure s = f ⁻¹' closure (f '' s) :=
  by
  ext x
  rw [Set.mem_preimage, ← closure_induced, hf.eq_induced]

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

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

Разделы

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

Аффилиация

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