α : Type u
β : Type v
ι : Type ?u.51065
π : ι → Type ?u.51070
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
⊢ HasBasis (⨅ (s : Set α) (_ : IsClosed s ∧ IsCompact s), 𝓟 (sᶜ)) (fun s => IsClosed s ∧ IsCompact s) compl
α : Type u
β : Type v
ι : Type ?u.51065
π : ι → Type ?u.51070
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
⊢ HasBasis (coclosedCompact α) (fun s => IsClosed s ∧ IsCompact s) compl
simp only [Filter.coclosedCompact, iInf_and']
α : Type u
β : Type v
ι : Type ?u.51065
π : ι → Type ?u.51070
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
⊢ ∀ (i : Set α),
    IsClosed i ∧ IsCompact i →
      ∀ (j : Set α), IsClosed j ∧ IsCompact j → ∃ k, (IsClosed k ∧ IsCompact k) ∧ kᶜ ⊆ iᶜ ∧ kᶜ ⊆ jᶜ
α : Type u
β : Type v
ι : Type ?u.51065
π : ι → Type ?u.51070
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
⊢ HasBasis (⨅ (s : Set α) (_ : IsClosed s ∧ IsCompact s), 𝓟 (sᶜ)) (fun s => IsClosed s ∧ IsCompact s) compl
refine' hasBasis_biInf_principal' _ ⟨∅, isClosed_empty, isCompact_empty⟩
case intro.intro
α : Type u
β : Type v
ι : Type ?u.51065
π : ι → Type ?u.51070
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
hs₁ : IsClosed s
hs₂ : IsCompact s
t : Set α
ht₁ : IsClosed t
ht₂ : IsCompact t
⊢ ∃ k, (IsClosed k ∧ IsCompact k) ∧ kᶜ ⊆ sᶜ ∧ kᶜ ⊆ tᶜ
α : Type u
β : Type v
ι : Type ?u.51065
π : ι → Type ?u.51070
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
⊢ ∀ (i : Set α),
    IsClosed i ∧ IsCompact i →
      ∀ (j : Set α), IsClosed j ∧ IsCompact j → ∃ k, (IsClosed k ∧ IsCompact k) ∧ kᶜ ⊆ iᶜ ∧ kᶜ ⊆ jᶜ
rintro s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩
no goals
case intro.intro
α : Type u
β : Type v
ι : Type ?u.51065
π : ι → Type ?u.51070
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
hs₁ : IsClosed s
hs₂ : IsCompact s
t : Set α
ht₁ : IsClosed t
ht₂ : IsCompact t
⊢ ∃ k, (IsClosed k ∧ IsCompact k) ∧ kᶜ ⊆ sᶜ ∧ kᶜ ⊆ tᶜ
exact ⟨s ∪ t, ⟨⟨hs₁.union ht₁, hs₂.union ht₂⟩, compl_subset_compl.2 (subset_union_left _ _),
  compl_subset_compl.2 (subset_union_right _ _)⟩⟩