α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
⊢ sᶜ ∈ coclosedCompact α ↔ IsCompact (closure s)
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
⊢ IsBounded s ↔ IsCompact (closure s)
change sᶜ ∈ Filter.coclosedCompact α ↔ _
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
⊢ (∃ t, IsClosed t ∧ IsCompact t ∧ tᶜ ⊆ sᶜ) ↔ IsCompact (closure s)
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
⊢ sᶜ ∈ coclosedCompact α ↔ IsCompact (closure s)
rw [Filter.mem_coclosedCompact]
case mp
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
⊢ (∃ t, IsClosed t ∧ IsCompact t ∧ tᶜ ⊆ sᶜ) → IsCompact (closure s)

case mpr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
⊢ IsCompact (closure s) → ∃ t, IsClosed t ∧ IsCompact t ∧ tᶜ ⊆ sᶜ
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
⊢ (∃ t, IsClosed t ∧ IsCompact t ∧ tᶜ ⊆ sᶜ) ↔ IsCompact (closure s)
constructor
case mp.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
ht₁ : IsClosed t
ht₂ : IsCompact t
hst : tᶜ ⊆ sᶜ
⊢ IsCompact (closure s)
case mp
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
⊢ (∃ t, IsClosed t ∧ IsCompact t ∧ tᶜ ⊆ sᶜ) → IsCompact (closure s)
rintro ⟨t, ht₁, ht₂, hst⟩
case mp.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
ht₁ : IsClosed t
ht₂ : IsCompact t
hst : s ⊆ t
⊢ IsCompact (closure s)
case mp.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
ht₁ : IsClosed t
ht₂ : IsCompact t
hst : tᶜ ⊆ sᶜ
⊢ IsCompact (closure s)
rw [compl_subset_compl] at hst
no goals
case mp.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
ht₁ : IsClosed t
ht₂ : IsCompact t
hst : s ⊆ t
⊢ IsCompact (closure s)
exact isCompact_of_isClosed_subset ht₂ isClosed_closure (closure_minimal hst ht₁)
case mpr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
h : IsCompact (closure s)
⊢ ∃ t, IsClosed t ∧ IsCompact t ∧ tᶜ ⊆ sᶜ
case mpr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
⊢ IsCompact (closure s) → ∃ t, IsClosed t ∧ IsCompact t ∧ tᶜ ⊆ sᶜ
intro h
no goals
case mpr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
h : IsCompact (closure s)
⊢ ∃ t, IsClosed t ∧ IsCompact t ∧ tᶜ ⊆ sᶜ
exact ⟨closure s, isClosed_closure, h, compl_subset_compl.mpr subset_closure⟩