case intro.intro.intro.intro
α : Type u_1
β : Type ?u.67736
inst✝ : TopologicalSpace α
s : Set α
t : TopologicalSpace α
t_le : t ≤ inst✝
t_polish : PolishSpace α
h : IsClosed s
h' : IsOpen s
⊢ IsClopenable (sᶜ)
α : Type u_1
β : Type ?u.67736
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopenable s
⊢ IsClopenable (sᶜ)
rcases hs with ⟨t, t_le, t_polish, h, h'⟩
no goals
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.67736
inst✝ : TopologicalSpace α
s : Set α
t : TopologicalSpace α
t_le : t ≤ inst✝
t_polish : PolishSpace α
h : IsClosed s
h' : IsOpen s
⊢ IsClopenable (sᶜ)
exact ⟨t, t_le, t_polish, @IsOpen.isClosed_compl α t s h', @IsClosed.isOpen_compl α t s h⟩