α : Type u
β : Type v
ι : Type ?u.53826
π : ι → Type ?u.53831
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
⊢ sᶜ ∈ cocompact α ↔ ∃ t, IsCompact t ∧ s ⊆ t
α : Type u
β : Type v
ι : Type ?u.53826
π : ι → Type ?u.53831
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
⊢ IsBounded s ↔ ∃ t, IsCompact t ∧ s ⊆ t
change sᶜ ∈ Filter.cocompact α ↔ _
α : Type u
β : Type v
ι : Type ?u.53826
π : ι → Type ?u.53831
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
⊢ (∃ t, IsCompact t ∧ tᶜ ⊆ sᶜ) ↔ ∃ t, IsCompact t ∧ s ⊆ t
α : Type u
β : Type v
ι : Type ?u.53826
π : ι → Type ?u.53831
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
⊢ sᶜ ∈ cocompact α ↔ ∃ t, IsCompact t ∧ s ⊆ t
rw [Filter.mem_cocompact]
no goals
α : Type u
β : Type v
ι : Type ?u.53826
π : ι → Type ?u.53831
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
⊢ (∃ t, IsCompact t ∧ tᶜ ⊆ sᶜ) ↔ ∃ t, IsCompact t ∧ s ⊆ t
simp