isClosed_preimage_val_coborder

Mathlib.Topology.LocallyClosed

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

← MathLib Explorer

English

The set coborder s ∩ s (as a subset of the ambient space) is closed.

Русский

Множество coborder s ∩ s (как подмножество пространства) является закрытым.

LaTeX

$$$\text{IsClosed}(\operatorname{coborder}(s) \cap s)$$$

Lean4

theorem isClosed_preimage_val_coborder : IsClosed (coborder s ↓∩ s) := by
  rw [isClosed_preimage_val, inter_eq_right.mpr subset_coborder, coborder_inter_closure]

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

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

Разделы

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

Аффилиация

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