isOpen_right_of_isOpen_union

Mathlib.Topology.Separation.SeparatedNhds

URI: https://scilib.ai/kg/mathlib#SeparatedNhds.isOpen_right_of_isOpen_union

← MathLib Explorer

English

If SeparatedNhds s t and s ∪ t is open, then t is open.

Русский

Если SeparatedNhds s t и s ∪ t открыто, то t открыто.

LaTeX

$$$\\text{SeparatedNhds } s t \\land IsOpen (s \\cup t) \\Rightarrow IsOpen t.$$$

Lean4

theorem isOpen_right_of_isOpen_union (hst : SeparatedNhds s t) (hst' : IsOpen (s ∪ t)) : IsOpen t :=
  hst.symm.isOpen_left_of_isOpen_union (union_comm _ _ ▸ hst')

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

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

Разделы

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

Аффилиация

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