α : Type u
β : Type v
ι : Type ?u.1517
π : ι → Type ?u.1522
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
hs : IsCompact s
p : Set α → Prop
he : p ∅
hmono : ∀ ⦃s t : Set α⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set α⦄, p s → p t → p (s ∪ t)
hnhds : ∀ (x : α), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ p t
f : Filter α :=
  { sets := {t | p (tᶜ)}, univ_sets := (_ : univ ∈ {t | p (tᶜ)}),
    sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ {t | p (tᶜ)} → x ⊆ y → p (yᶜ)),
    inter_sets := (_ : ∀ {x y : Set α}, x ∈ {t | p (tᶜ)} → y ∈ {t | p (tᶜ)} → p ((x ∩ y)ᶜ)) }
⊢ p s
α : Type u
β : Type v
ι : Type ?u.1517
π : ι → Type ?u.1522
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
hs : IsCompact s
p : Set α → Prop
he : p ∅
hmono : ∀ ⦃s t : Set α⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set α⦄, p s → p t → p (s ∪ t)
hnhds : ∀ (x : α), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ p t
⊢ p s
let f : Filter α :=
  { sets := { t | p (tᶜ) }
    univ_sets := by simpa
    sets_of_superset := fun ht₁ ht => hmono (compl_subset_compl.2 ht) ht₁
    inter_sets := fun ht₁ ht₂ => by simp [compl_inter, hunion ht₁ ht₂] }
α : Type u
β : Type v
ι : Type ?u.1517
π : ι → Type ?u.1522
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
hs : IsCompact s
p : Set α → Prop
he : p ∅
hmono : ∀ ⦃s t : Set α⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set α⦄, p s → p t → p (s ∪ t)
hnhds : ∀ (x : α), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ p t
f : Filter α :=
  { sets := {t | p (tᶜ)}, univ_sets := (_ : univ ∈ {t | p (tᶜ)}),
    sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ {t | p (tᶜ)} → x ⊆ y → p (yᶜ)),
    inter_sets := (_ : ∀ {x y : Set α}, x ∈ {t | p (tᶜ)} → y ∈ {t | p (tᶜ)} → p ((x ∩ y)ᶜ)) }
this : sᶜ ∈ f
⊢ p s
α : Type u
β : Type v
ι : Type ?u.1517
π : ι → Type ?u.1522
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
hs : IsCompact s
p : Set α → Prop
he : p ∅
hmono : ∀ ⦃s t : Set α⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set α⦄, p s → p t → p (s ∪ t)
hnhds : ∀ (x : α), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ p t
f : Filter α :=
  { sets := {t | p (tᶜ)}, univ_sets := (_ : univ ∈ {t | p (tᶜ)}),
    sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ {t | p (tᶜ)} → x ⊆ y → p (yᶜ)),
    inter_sets := (_ : ∀ {x y : Set α}, x ∈ {t | p (tᶜ)} → y ∈ {t | p (tᶜ)} → p ((x ∩ y)ᶜ)) }
⊢ p s
have : sᶜ ∈ f := hs.compl_mem_sets_of_nhdsWithin (by simpa using hnhds)
no goals
α : Type u
β : Type v
ι : Type ?u.1517
π : ι → Type ?u.1522
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
hs : IsCompact s
p : Set α → Prop
he : p ∅
hmono : ∀ ⦃s t : Set α⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set α⦄, p s → p t → p (s ∪ t)
hnhds : ∀ (x : α), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ p t
f : Filter α :=
  { sets := {t | p (tᶜ)}, univ_sets := (_ : univ ∈ {t | p (tᶜ)}),
    sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ {t | p (tᶜ)} → x ⊆ y → p (yᶜ)),
    inter_sets := (_ : ∀ {x y : Set α}, x ∈ {t | p (tᶜ)} → y ∈ {t | p (tᶜ)} → p ((x ∩ y)ᶜ)) }
this : sᶜ ∈ f
⊢ p s
rwa [← compl_compl s]
no goals
α : Type u
β : Type v
ι : Type ?u.1517
π : ι → Type ?u.1522
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
hs : IsCompact s
p : Set α → Prop
he : p ∅
hmono : ∀ ⦃s t : Set α⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set α⦄, p s → p t → p (s ∪ t)
hnhds : ∀ (x : α), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ p t
⊢ univ ∈ {t | p (tᶜ)}
simpa
no goals
α : Type u
β : Type v
ι : Type ?u.1517
π : ι → Type ?u.1522
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
hs : IsCompact s
p : Set α → Prop
he : p ∅
hmono : ∀ ⦃s t : Set α⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set α⦄, p s → p t → p (s ∪ t)
hnhds : ∀ (x : α), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ p t
x✝ y✝ : Set α
ht₁ : x✝ ∈ {t | p (tᶜ)}
ht₂ : y✝ ∈ {t | p (tᶜ)}
⊢ x✝ ∩ y✝ ∈ {t | p (tᶜ)}
simp [compl_inter, hunion ht₁ ht₂]
no goals
α : Type u
β : Type v
ι : Type ?u.1517
π : ι → Type ?u.1522
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
hs : IsCompact s
p : Set α → Prop
he : p ∅
hmono : ∀ ⦃s t : Set α⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set α⦄, p s → p t → p (s ∪ t)
hnhds : ∀ (x : α), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ p t
f : Filter α :=
  { sets := {t | p (tᶜ)}, univ_sets := (_ : univ ∈ {t | p (tᶜ)}),
    sets_of_superset := (_ : ∀ {x y : Set α}, x ∈ {t | p (tᶜ)} → x ⊆ y → p (yᶜ)),
    inter_sets := (_ : ∀ {x y : Set α}, x ∈ {t | p (tᶜ)} → y ∈ {t | p (tᶜ)} → p ((x ∩ y)ᶜ)) }
⊢ ∀ (a : α), a ∈ s → ∃ t, t ∈ 𝓝[s] a ∧ tᶜ ∈ f
simpa using hnhds