α : Type u
β : Type v
ι : Type ?u.33227
π : ι → Type ?u.33232
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
inst✝ : DiscreteTopology α
s : Set α
hs : IsCompact s
this : ∀ (x : α), {x} ∈ 𝓝 x
⊢ Set.Finite s
α : Type u
β : Type v
ι : Type ?u.33227
π : ι → Type ?u.33232
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
inst✝ : DiscreteTopology α
s : Set α
hs : IsCompact s
⊢ Set.Finite s
have : ∀ x : α, ({x} : Set α) ∈ 𝓝 x := by simp [nhds_discrete]
case intro.intro
α : Type u
β : Type v
ι : Type ?u.33227
π : ι → Type ?u.33232
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t✝ : Set α
inst✝ : DiscreteTopology α
s : Set α
hs : IsCompact s
this : ∀ (x : α), {x} ∈ 𝓝 x
t : Finset α
left✝ : ∀ (x : α), x ∈ t → x ∈ s
hst : s ⊆ ⋃ (x : α) (_ : x ∈ t), {x}
⊢ Set.Finite s
α : Type u
β : Type v
ι : Type ?u.33227
π : ι → Type ?u.33232
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
inst✝ : DiscreteTopology α
s : Set α
hs : IsCompact s
this : ∀ (x : α), {x} ∈ 𝓝 x
⊢ Set.Finite s
rcases hs.elim_nhds_subcover (fun x => {x}) fun x _ => this x with ⟨t, _, hst⟩
case intro.intro
α : Type u
β : Type v
ι : Type ?u.33227
π : ι → Type ?u.33232
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t✝ : Set α
inst✝ : DiscreteTopology α
s : Set α
hs : IsCompact s
this : ∀ (x : α), {x} ∈ 𝓝 x
t : Finset α
left✝ : ∀ (x : α), x ∈ t → x ∈ s
hst : s ⊆ ↑t
⊢ Set.Finite s
case intro.intro
α : Type u
β : Type v
ι : Type ?u.33227
π : ι → Type ?u.33232
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t✝ : Set α
inst✝ : DiscreteTopology α
s : Set α
hs : IsCompact s
this : ∀ (x : α), {x} ∈ 𝓝 x
t : Finset α
left✝ : ∀ (x : α), x ∈ t → x ∈ s
hst : s ⊆ ⋃ (x : α) (_ : x ∈ t), {x}
⊢ Set.Finite s
simp only [← t.set_biUnion_coe, biUnion_of_singleton] at hst
no goals
case intro.intro
α : Type u
β : Type v
ι : Type ?u.33227
π : ι → Type ?u.33232
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t✝ : Set α
inst✝ : DiscreteTopology α
s : Set α
hs : IsCompact s
this : ∀ (x : α), {x} ∈ 𝓝 x
t : Finset α
left✝ : ∀ (x : α), x ∈ t → x ∈ s
hst : s ⊆ ↑t
⊢ Set.Finite s
exact t.finite_toSet.subset hst
no goals
α : Type u
β : Type v
ι : Type ?u.33227
π : ι → Type ?u.33232
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
inst✝ : DiscreteTopology α
s : Set α
hs : IsCompact s
⊢ ∀ (x : α), {x} ∈ 𝓝 x
simp [nhds_discrete]