isClopenable — Mathlib

English

Every open set in a Polish space is clopenable.

Русский

Каждое открытое множество в полиспейсе можно сделать открытым и замкнутым в более тонкой топологии.

LaTeX

$$$\text{IsOpen}(s) \Rightarrow \text{IsClopenable}(s)$$$

Lean4

theorem _root_.IsOpen.isClopenable [TopologicalSpace α] [PolishSpace α] {s : Set α} (hs : IsOpen s) : IsClopenable s :=
  by simpa using hs.isClosed_compl.isClopenable.compl

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