coe_map

Mathlib.Topology.Sets.Compacts

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.CompactOpens.coe_map

← MathLib Explorer

English

The underlying set of the image equals the image of the underlying set.

Русский

Базисное множество образа равно изображению базисного множества.

LaTeX

$$$\uparrow (s.map f hf hf') = f '' \uparrow s$$$

Lean4

@[simp, norm_cast]
theorem coe_map {f : α → β} (hf : Continuous f) (hf' : IsOpenMap f) (s : CompactOpens α) :
    (s.map f hf hf' : Set β) = f '' s :=
  rfl

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

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

Разделы

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

Аффилиация

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