α : Type u
β : Type v
ι : Type ?u.95561
π : ι → Type ?u.95566
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
hs : IsCompact s
hs' : Set.Infinite s
H : ∀ (z : α), z ∈ s → ¬NeBot (𝓝[{z}ᶜ] z ⊓ 𝓟 s)
⊢ False
α : Type u
β : Type v
ι : Type ?u.95561
π : ι → Type ?u.95566
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
hs : IsCompact s
hs' : Set.Infinite s
⊢ ∃ z, z ∈ s ∧ NeBot (𝓝[{z}ᶜ] z ⊓ 𝓟 s)
by_contra' H
α : Type u
β : Type v
ι : Type ?u.95561
π : ι → Type ?u.95566
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
hs : IsCompact s
hs' : Set.Infinite s
H : ∀ (z : α), z ∈ s → 𝓝[{z}ᶜ] z ⊓ 𝓟 s = ⊥
⊢ False
α : Type u
β : Type v
ι : Type ?u.95561
π : ι → Type ?u.95566
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
hs : IsCompact s
hs' : Set.Infinite s
H : ∀ (z : α), z ∈ s → ¬NeBot (𝓝[{z}ᶜ] z ⊓ 𝓟 s)
⊢ False
simp_rw [not_neBot] at H
no goals
α : Type u
β : Type v
ι : Type ?u.95561
π : ι → Type ?u.95566
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
hs : IsCompact s
hs' : Set.Infinite s
H : ∀ (z : α), z ∈ s → 𝓝[{z}ᶜ] z ⊓ 𝓟 s = ⊥
⊢ False
exact hs' (hs.finite <| discreteTopology_subtype_iff.mpr H)