feat(topology/lindelof): define Lindelöf space

src/geometry/manifold/charted_space.lean

@@ -497,6 +497,8 @@ variables (H) [topological_space H] [topological_space M] [charted_space H M]
 lemma mem_chart_target (x : M) : chart_at H x x ∈ (chart_at H x).target :=
 (chart_at H x).map_source (mem_chart_source _ _)
 
+variable (M)
+
 /-- If a topological space admits an atlas with locally compact charts, then the space itself
 is locally compact. -/
 lemma charted_space.locally_compact [locally_compact_space H] : locally_compact_space M :=
@@ -527,16 +529,21 @@ begin
   exact second_countable_topology_of_countable_cover (λ x : s, (chart_at H (x : M)).open_source) hs
 end
 
-lemma charted_space.second_countable_of_sigma_compact [second_countable_topology H]
-  [sigma_compact_space M] :
+lemma charted_space.second_countable_of_lindelof [second_countable_topology H] [lindelof_space M] :
   second_countable_topology M :=
 begin
   obtain ⟨s, hsc, hsU⟩ : ∃ s, countable s ∧ (⋃ x (hx : x ∈ s), (chart_at H x).source) = univ :=
-    countable_cover_nhds_of_sigma_compact
-      (λ x : M, is_open.mem_nhds (chart_at H x).open_source (mem_chart_source H x)),
+    countable_cover_nhds (λ x : M, (chart_at H x).open_source.mem_nhds (mem_chart_source H x)),
   exact charted_space.second_countable_of_countable_cover H hsU hsc
 end
 
+lemma charted_space.sigma_compact_of_lindelof [locally_compact_space H] [lindelof_space M] :
+  sigma_compact_space M :=
+begin
+  haveI := charted_space.locally_compact H M,
+  exact sigma_compact_space_of_locally_compact_lindelof M
+end
+
 end
 
 /-- For technical reasons we introduce two type tags:

src/geometry/manifold/partition_of_unity.lean

@@ -90,7 +90,7 @@ variables (ι M)
 * for each point `x ∈ s` there exists `i` such that `f i =ᶠ[𝓝 x] 1`;
   in other words, `x` belongs to the interior of `{y | f i y = 1}`;
 
-If `M` is a finite dimensional real manifold which is a sigma-compact Hausdorff topological space,
+If `M` is a finite dimensional real manifold which is a `σ`-compact Hausdorff topological space,
 then for every covering `U : M → set M`, `∀ x, U x ∈ 𝓝 x`, there exists a `smooth_bump_covering`
 subordinate to `U`, see `smooth_bump_covering.exists_is_subordinate`.
 
@@ -242,7 +242,7 @@ lemma exists_is_subordinate [t2_space M] [sigma_compact_space M] (hs : is_closed
 begin
   -- First we deduce some missing instances
   haveI : locally_compact_space H := I.locally_compact,
-  haveI : locally_compact_space M := charted_space.locally_compact H,
+  haveI : locally_compact_space M := charted_space.locally_compact H M,
   haveI : normal_space M := normal_of_paracompact_t2,
   -- Next we choose a covering by supports of smooth bump functions
   have hB := λ x hx, smooth_bump_function.nhds_basis_support I (hU x hx),
@@ -401,7 +401,7 @@ lemma exists_is_subordinate {s : set M} (hs : is_closed s) (U : ι → set M) (h
   ∃ f : smooth_partition_of_unity ι I M s, f.is_subordinate U :=
 begin
   haveI : locally_compact_space H := I.locally_compact,
-  haveI : locally_compact_space M := charted_space.locally_compact H,
+  haveI : locally_compact_space M := charted_space.locally_compact H M,
   haveI : normal_space M := normal_of_paracompact_t2,
   rcases bump_covering.exists_is_subordinate_of_prop (smooth I 𝓘(ℝ)) _ hs U ho hU
     with ⟨f, hf, hfU⟩,

src/geometry/manifold/smooth_manifold_with_corners.lean

@@ -263,6 +263,10 @@ protected lemma second_countable_topology [second_countable_topology E]
   (I : model_with_corners 𝕜 E H) : second_countable_topology H :=
 I.closed_embedding.to_embedding.second_countable_topology
 
+protected lemma lindelof_space [lindelof_space E]
+  (I : model_with_corners 𝕜 E H) : lindelof_space H :=
+I.closed_embedding.lindelof_space
+
 end model_with_corners
 
 section

src/measure_theory/measure/measure_space.lean

@@ -2811,11 +2811,11 @@ omit m0
 
 @[priority 100] -- see Note [lower instance priority]
 instance sigma_finite_of_locally_finite [topological_space α]
-  [second_countable_topology α] [is_locally_finite_measure μ] :
+  [lindelof_space α] [is_locally_finite_measure μ] :
   sigma_finite μ :=
 begin
   choose s hsx hsμ using μ.finite_at_nhds,
-  rcases topological_space.countable_cover_nhds hsx with ⟨t, htc, htU⟩,
+  rcases countable_cover_nhds hsx with ⟨t, htc, htU⟩,
   refine measure.sigma_finite_of_countable (htc.image s) (ball_image_iff.2 $ λ x hx, hsμ x) _,
   rwa sUnion_image
 end
@@ -2831,6 +2831,11 @@ lemma is_locally_finite_measure_of_is_finite_measure_on_compacts [topological_sp
   exact ⟨K, K_mem, K_compact.measure_lt_top⟩,
 end⟩
 
+lemma _root_.is_lindelof.measure_null_of_locally_null [topological_space α]
+  {s : set α} (hs : is_lindelof s) (hsμ : ∀ x ∈ s, ∃ u ∈ 𝓝[s] x, μ u = 0) :
+  μ s = 0 :=
+hs.outer_measure_null_of_locally_null μ.to_outer_measure hsμ
+
 lemma exists_pos_measure_of_cover [encodable ι] {U : ι → set α} (hU : (⋃ i, U i) = univ)
   (hμ : μ ≠ 0) : ∃ i, 0 < μ (U i) :=
 begin
@@ -2849,7 +2854,7 @@ exists_pos_preimage_ball id x hμ
 
 /-- If a set has zero measure in a neighborhood of each of its points, then it has zero measure
 in a second-countable space. -/
-lemma null_of_locally_null [topological_space α] [second_countable_topology α]
+lemma null_of_locally_null [topological_space α] [strongly_lindelof_space α]
   (s : set α) (hs : ∀ x ∈ s, ∃ u ∈ 𝓝[s] x, μ u = 0) :
   μ s = 0 :=
 μ.to_outer_measure.null_of_locally_null s hs

src/measure_theory/measure/outer_measure.lean

@@ -115,19 +115,24 @@ protected lemma union (m : outer_measure α) (s₁ s₂ : set α) :
   m (s₁ ∪ s₂) ≤ m s₁ + m s₂ :=
 rel_sup_add m m.empty (≤) m.Union_nat s₁ s₂
 
-/-- If a set has zero measure in a neighborhood of each of its points, then it has zero measure
-in a second-countable space. -/
-lemma null_of_locally_null [topological_space α] [second_countable_topology α] (m : outer_measure α)
-  (s : set α) (hs : ∀ x ∈ s, ∃ u ∈ 𝓝[s] x, m u = 0) :
+lemma _root_.is_lindelof.outer_measure_null_of_locally_null [topological_space α]
+  {s : set α} (hs : is_lindelof s) (m : outer_measure α) (hsm : ∀ x ∈ s, ∃ u ∈ 𝓝[s] x, m u = 0) :
   m s = 0 :=
 begin
-  choose! u hxu hu₀ using hs,
+  choose! u hxu hu₀ using hsm,
   obtain ⟨t, ts, t_count, ht⟩ : ∃ t ⊆ s, t.countable ∧ s ⊆ ⋃ x ∈ t, u x :=
-    topological_space.countable_cover_nhds_within hxu,
+    hs.countable_cover_nhds_within hxu,
   apply m.mono_null ht,
   exact (m.bUnion_null_iff t_count).2 (λ x hx, hu₀ x (ts hx))
 end
 
+/-- If a set has zero measure in a neighborhood of each of its points, then it has zero measure
+in a second-countable space. -/
+lemma null_of_locally_null [topological_space α] [strongly_lindelof_space α] (m : outer_measure α)
+  (s : set α) (hs : ∀ x ∈ s, ∃ u ∈ 𝓝[s] x, m u = 0) :
+  m s = 0 :=
+s.is_lindelof.outer_measure_null_of_locally_null m hs
+
 /-- If `m s ≠ 0`, then for some point `x ∈ s` and any `t ∈ 𝓝[s] x` we have `0 < m t`. -/
 lemma exists_mem_forall_mem_nhds_within_pos [topological_space α] [second_countable_topology α]
   (m : outer_measure α) {s : set α} (hs : m s ≠ 0) :

src/topology/bases.lean

@@ -21,20 +21,20 @@ conditions are equivalent in this case).
 
 ## Main definitions
 
-* `is_topological_basis s`: The topological space `t` has basis `s`.
-* `separable_space α`: The topological space `t` has a countable, dense subset.
-* `is_separable s`: The set `s` is contained in the closure of a countable set.
-* `first_countable_topology α`: A topology in which `𝓝 x` is countably generated for every `x`.
-* `second_countable_topology α`: A topology which has a topological basis which is countable.
+* `topological_space.is_topological_basis s`: The topological space `t` has basis `s`.
+* `topological_space.separable_space α`: The topological space `t` has a countable, dense subset.
+* `topological_space.is_separable s`: The set `s` is contained in the closure of a countable set.
+* `topological_space.first_countable_topology α`: A topology in which `𝓝 x` is countably generated
+  for every `x`.
+* `topological_space.second_countable_topology α`: A topology which has a topological basis which is
+  countable.
 
 ## Main results
 
-* `first_countable_topology.tendsto_subseq`: In a first-countable space,
+* `topological_space.first_countable_topology.tendsto_subseq`: In a first-countable space,
   cluster points are limits of subsequences.
-* `second_countable_topology.is_open_Union_countable`: In a second-countable space, the union of
+* `topological_space.is_open_Union_countable`: In a second-countable space, the union of
   arbitrarily-many open sets is equal to a sub-union of only countably many of these sets.
-* `second_countable_topology.countable_cover_nhds`: Consider `f : α → set α` with the property that
-  `f x ∈ 𝓝 x` for all `x`. Then there is some countable set `s` whose image covers the space.
 
 ## Implementation Notes
 For our applications we are interested that there exists a countable basis, but we do not need the
@@ -673,52 +673,6 @@ begin
     (countable_Union $ λ i, (countable_countable_basis _).image _)
 end
 
-/-- In a second-countable space, an open set, given as a union of open sets,
-is equal to the union of countably many of those sets. -/
-lemma is_open_Union_countable [second_countable_topology α]
-  {ι} (s : ι → set α) (H : ∀ i, is_open (s i)) :
-  ∃ T : set ι, countable T ∧ (⋃ i ∈ T, s i) = ⋃ i, s i :=
-begin
-  let B := {b ∈ countable_basis α | ∃ i, b ⊆ s i},
-  choose f hf using λ b : B, b.2.2,
-  haveI : encodable B := ((countable_countable_basis α).mono (sep_subset _ _)).to_encodable,
-  refine ⟨_, countable_range f, (Union₂_subset_Union _ _).antisymm (sUnion_subset _)⟩,
-  rintro _ ⟨i, rfl⟩ x xs,
-  rcases (is_basis_countable_basis α).exists_subset_of_mem_open xs (H _) with ⟨b, hb, xb, bs⟩,
-  exact ⟨_, ⟨_, rfl⟩, _, ⟨⟨⟨_, hb, _, bs⟩, rfl⟩, rfl⟩, hf _ (by exact xb)⟩
-end
-
-lemma is_open_sUnion_countable [second_countable_topology α]
-  (S : set (set α)) (H : ∀ s ∈ S, is_open s) :
-  ∃ T : set (set α), countable T ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S :=
-let ⟨T, cT, hT⟩ := is_open_Union_countable (λ s:S, s.1) (λ s, H s.1 s.2) in
-⟨subtype.val '' T, cT.image _,
-  image_subset_iff.2 $ λ ⟨x, xs⟩ xt, xs,
-  by rwa [sUnion_image, sUnion_eq_Union]⟩
-
-/-- In a topological space with second countable topology, if `f` is a function that sends each
-point `x` to a neighborhood of `x`, then for some countable set `s`, the neighborhoods `f x`,
-`x ∈ s`, cover the whole space. -/
-lemma countable_cover_nhds [second_countable_topology α] {f : α → set α}
-  (hf : ∀ x, f x ∈ 𝓝 x) : ∃ s : set α, countable s ∧ (⋃ x ∈ s, f x) = univ :=
-begin
-  rcases is_open_Union_countable (λ x, interior (f x)) (λ x, is_open_interior) with ⟨s, hsc, hsU⟩,
-  suffices : (⋃ x ∈ s, interior (f x)) = univ,
-    from ⟨s, hsc, flip eq_univ_of_subset this $ Union₂_mono $ λ _ _, interior_subset⟩,
-  simp only [hsU, eq_univ_iff_forall, mem_Union],
-  exact λ x, ⟨x, mem_interior_iff_mem_nhds.2 (hf x)⟩
-end
-
-lemma countable_cover_nhds_within [second_countable_topology α] {f : α → set α} {s : set α}
-  (hf : ∀ x ∈ s, f x ∈ 𝓝[s] x) : ∃ t ⊆ s, countable t ∧ s ⊆ (⋃ x ∈ t, f x) :=
-begin
-  have : ∀ x : s, coe ⁻¹' (f x) ∈ 𝓝 x, from λ x, preimage_coe_mem_nhds_subtype.2 (hf x x.2),
-  rcases countable_cover_nhds this with ⟨t, htc, htU⟩,
-  refine ⟨coe '' t, subtype.coe_image_subset _ _, htc.image _, λ x hx, _⟩,
-  simp only [bUnion_image, eq_univ_iff_forall, ← preimage_Union, mem_preimage] at htU ⊢,
-  exact htU ⟨x, hx⟩
-end
-
 section sigma
 
 variables {ι : Type*} {E : ι → Type*} [∀ i, topological_space (E i)]