coborder_mem_residual

Mathlib.Topology.Baire.BaireMeasurable

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

← MathLib Explorer

English

If s is locally closed, then coborder(s) belongs to the residual filter on α.

Русский

Если s локально замкнуто, то coborder(s) принадлежит резидуальному фильтру на α.

LaTeX

$$$$ \text{coborder}(s) \in \text{residual}(\alpha). $$$$

Lean4

theorem coborder_mem_residual {s : Set α} (hs : IsLocallyClosed s) : coborder s ∈ residual α :=
  residual_of_dense_open hs.isOpen_coborder dense_coborder

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

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

Разделы

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

Аффилиация

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