α✝ : Type u
β : Type v
ι : Type ?u.87095
π : ι → Type ?u.87100
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalSpace β
s t : Set α✝
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : Infinite α
H : ∀ (z : α), ¬NeBot (𝓝[{z}ᶜ] z)
⊢ False
α✝ : Type u
β : Type v
ι : Type ?u.87095
π : ι → Type ?u.87100
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalSpace β
s t : Set α✝
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : Infinite α
⊢ ∃ z, NeBot (𝓝[{z}ᶜ] z)
by_contra' H
α✝ : Type u
β : Type v
ι : Type ?u.87095
π : ι → Type ?u.87100
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalSpace β
s t : Set α✝
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : Infinite α
H : ∀ (z : α), 𝓝[{z}ᶜ] z = ⊥
⊢ False
α✝ : Type u
β : Type v
ι : Type ?u.87095
π : ι → Type ?u.87100
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalSpace β
s t : Set α✝
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : Infinite α
H : ∀ (z : α), ¬NeBot (𝓝[{z}ᶜ] z)
⊢ False
simp_rw [not_neBot] at H
α✝ : Type u
β : Type v
ι : Type ?u.87095
π : ι → Type ?u.87100
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalSpace β
s t : Set α✝
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : Infinite α
H : ∀ (z : α), 𝓝[{z}ᶜ] z = ⊥
this : DiscreteTopology α
⊢ False
α✝ : Type u
β : Type v
ι : Type ?u.87095
π : ι → Type ?u.87100
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalSpace β
s t : Set α✝
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : Infinite α
H : ∀ (z : α), 𝓝[{z}ᶜ] z = ⊥
⊢ False
haveI := discreteTopology_iff_nhds_ne.2 H
no goals
α✝ : Type u
β : Type v
ι : Type ?u.87095
π : ι → Type ?u.87100
inst✝⁴ : TopologicalSpace α✝
inst✝³ : TopologicalSpace β
s t : Set α✝
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : Infinite α
H : ∀ (z : α), 𝓝[{z}ᶜ] z = ⊥
this : DiscreteTopology α
⊢ False
exact Infinite.not_finite (finite_of_compact_of_discrete : Finite α)