compl — Mathlib

English

If s is clopenable in a Polish space, so is its complement.

Русский

Если s — clopenable в полиспейс, то и его дополнение clopenable.

LaTeX

$$$\text{PolishSpace.IsClopenable}(s) \Rightarrow \text{PolishSpace.IsClopenable}(s^c)$$$

Lean4

theorem compl [TopologicalSpace α] {s : Set α} (hs : IsClopenable s) : IsClopenable sᶜ :=
  by
  rcases hs with ⟨t, t_le, t_polish, h, h'⟩
  exact ⟨t, t_le, t_polish, @IsOpen.isClosed_compl α t s h', @IsClosed.isOpen_compl α t s h⟩

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