feat(topology/subset_properties): locally finite family on a compact …

…space is finite (#6352)

src/data/set/finite.lean

@@ -188,14 +188,9 @@ fintype.of_equiv α $ (equiv.set.univ α).symm
 theorem finite_univ [fintype α] : finite (@univ α) := ⟨set.fintype_univ⟩
 
 /-- If `(set.univ : set α)` is finite then `α` is a finite type. -/
-noncomputable
-def fintype_of_univ_finite (H : (univ : set α).finite ) :
+noncomputable def fintype_of_univ_finite (H : (univ : set α).finite ) :
   fintype α :=
-begin
-  choose t ht using H.exists_finset,
-  refine ⟨t, _⟩,
-  simpa only [set.mem_univ, iff_true] using ht
-end
+@fintype.of_equiv _ (univ : set α) H.fintype (equiv.set.univ _)
 
 lemma univ_finite_iff_nonempty_fintype :
   (univ : set α).finite ↔ nonempty (fintype α) :=
@@ -206,8 +201,7 @@ begin
 end
 
 theorem infinite_univ_iff : (@univ α).infinite ↔ _root_.infinite α :=
-⟨λ h₁, ⟨λ h₂, h₁ $ @finite_univ α h₂⟩,
-  λ ⟨h₁⟩ ⟨h₂⟩, h₁ $ @fintype.of_equiv _ _ h₂ $ equiv.set.univ _⟩
+⟨λ h₁, ⟨λ h₂, h₁ $ @finite_univ α h₂⟩, λ ⟨h₁⟩ h₂, h₁ (fintype_of_univ_finite h₂)⟩
 
 theorem infinite_univ [h : _root_.infinite α] : infinite (@univ α) :=
 infinite_univ_iff.2 h

src/topology/basic.lean

@@ -922,7 +922,7 @@ le_nhds_Lim h
 end lim
 
 /-!
-### Locally finite families
+### Locally finite families
 -/
 
 /- locally finite family [General Topology (Bourbaki, 1995)] -/
@@ -933,8 +933,8 @@ section locally_finite
 def locally_finite (f : β → set α) :=
 ∀x:α, ∃t ∈ 𝓝 x, finite {i | (f i ∩ t).nonempty }
 
-lemma locally_finite_of_finite {f : β → set α} (h : finite (univ : set β)) : locally_finite f :=
-assume x, ⟨univ, univ_mem_sets, h.subset $ subset_univ _⟩
+lemma locally_finite_of_fintype [fintype β] (f : β → set α) : locally_finite f :=
+assume x, ⟨univ, univ_mem_sets, finite.of_fintype _⟩
 
 lemma locally_finite_subset
   {f₁ f₂ : β → set α} (hf₂ : locally_finite f₂) (hf : ∀b, f₁ b ⊆ f₂ b) : locally_finite f₁ :=

src/topology/subset_properties.lean

@@ -481,6 +481,46 @@ def fintype_of_compact_of_discrete [compact_space α] [discrete_topology α] :
   fintype α :=
 fintype_of_univ_finite $ finite_of_is_compact_of_discrete _ compact_univ
 
+lemma finite_cover_nhds_interior [compact_space α] {U : α → set α} (hU : ∀ x, U x ∈ 𝓝 x) :
+  ∃ t : finset α, (⋃ x ∈ t, interior (U x)) = univ :=
+let ⟨t, ht⟩ := compact_univ.elim_finite_subcover (λ x, interior (U x)) (λ x, is_open_interior)
+  (λ x _, mem_Union.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x)⟩)
+in ⟨t, univ_subset_iff.1 ht⟩
+
+lemma finite_cover_nhds [compact_space α] {U : α → set α} (hU : ∀ x, U x ∈ 𝓝 x) :
+  ∃ t : finset α, (⋃ x ∈ t, U x) = univ :=
+let ⟨t, ht⟩ := finite_cover_nhds_interior hU in ⟨t, univ_subset_iff.1 $
+  ht ▸ bUnion_subset_bUnion_right (λ x hx, interior_subset)⟩
+
+/-- If `α` is a compact space, then a locally finite family of sets of `α` can have only finitely
+many nonempty elements. -/
+lemma locally_finite.finite_nonempty_of_compact {ι : Type*} [compact_space α] {f : ι → set α}
+  (hf : locally_finite f) :
+  finite {i | (f i).nonempty} :=
+begin
+  choose U hxU hUf using hf,
+  rcases finite_cover_nhds hxU with ⟨t, ht⟩,
+  refine (t.finite_to_set.bUnion (λ x _, hUf x)).subset _,
+  rintro i ⟨x, hx⟩,
+  simp only [eq_univ_iff_forall, mem_Union] at ht ⊢,
+  rcases ht x with ⟨j, hjt, hjx⟩,
+  exact ⟨j, hjt, x, hx, hjx⟩
+end
+
+/-- If `α` is a compact space, then a locally finite family of nonempty sets of `α` can have only
+finitely many elements, `set.finite` version. -/
+lemma locally_finite.finite_of_compact {ι : Type*} [compact_space α] {f : ι → set α}
+  (hf : locally_finite f) (hne : ∀ i, (f i).nonempty) :
+  finite (univ : set ι) :=
+by simpa only [hne] using hf.finite_nonempty_of_compact
+
+/-- If `α` is a compact space, then a locally finite family of nonempty sets of `α` can have only
+finitely many elements, `fintype` version. -/
+noncomputable def locally_finite.fintype_of_compact {ι : Type*} [compact_space α] {f : ι → set α}
+  (hf : locally_finite f) (hne : ∀ i, (f i).nonempty) :
+  fintype ι :=
+fintype_of_univ_finite (hf.finite_of_compact hne)
+
 variables [topological_space β]
 
 lemma is_compact.image_of_continuous_on {f : α → β} (hs : is_compact s) (hf : continuous_on f s) :