From 8ac825d4079261d4c1396a623ee90e0aaeba85c1 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 26 Jan 2022 11:30:39 -0500 Subject: [PATCH 01/15] Snapshot --- src/data/set/lattice.lean | 59 ++---- src/order/bounded_order.lean | 3 + src/order/filter/basic.lean | 12 +- src/order/filter/countable_Inter.lean | 17 ++ src/topology/bases.lean | 4 +- src/topology/lindelof.lean | 283 ++++++++++++++++++++++++++ src/topology/metric_space/baire.lean | 14 +- 7 files changed, 331 insertions(+), 61 deletions(-) create mode 100644 src/topology/lindelof.lean diff --git a/src/data/set/lattice.lean b/src/data/set/lattice.lean index e38d60bc8fa3d..8b25751161b9b 100644 --- a/src/data/set/lattice.lean +++ b/src/data/set/lattice.lean @@ -67,7 +67,7 @@ instance : has_Sup (set α) := ⟨sUnion⟩ /-- Intersection of a set of sets. -/ def sInter (S : set (set α)) : set α := Inf S -prefix `⋂₀`:110 := sInter +prefix `⋂₀ `:110 := sInter @[simp] theorem mem_sInter {x : α} {S : set (set α)} : x ∈ ⋂₀ S ↔ ∀ t ∈ S, x ∈ t := iff.rfl @@ -701,12 +701,12 @@ theorem bUnion_union (s t : set α) (u : α → set β) : (⋃ x ∈ s ∪ t, u x) = (⋃ x ∈ s, u x) ∪ (⋃ x ∈ t, u x) := supr_union -@[simp] lemma Union_coe_set {α β : Type*} (s : set α) (f : α → set β) : - (⋃ (i : s), f i) = ⋃ (i ∈ s), f i := +@[simp] lemma Union_coe_set {α β : Type*} (s : set α) (f : s → set β) : + (⋃ i, f i) = ⋃ i ∈ s, f ⟨i, ‹i ∈ s›⟩ := Union_subtype _ _ -@[simp] lemma Inter_coe_set {α β : Type*} (s : set α) (f : α → set β) : - (⋂ (i : s), f i) = ⋂ (i ∈ s), f i := +@[simp] lemma Inter_coe_set {α β : Type*} (s : set α) (f : s → set β) : + (⋂ i, f i) = ⋂ i ∈ s, f ⟨i, ‹i ∈ s›⟩ := Inter_subtype _ _ theorem bUnion_insert (a : α) (s : set α) (t : α → set β) : @@ -785,13 +785,6 @@ theorem sUnion_union (S T : set (set α)) : ⋃₀ (S ∪ T) = ⋃₀ S ∪ ⋃ theorem sInter_union (S T : set (set α)) : ⋂₀ (S ∪ T) = ⋂₀ S ∩ ⋂₀ T := Inf_union -theorem sInter_Union (s : ι → set (set α)) : ⋂₀ (⋃ i, s i) = ⋂ i, ⋂₀ s i := -begin - ext x, - simp only [mem_Union, mem_Inter, mem_sInter, exists_imp_distrib], - split; tauto -end - @[simp] theorem sUnion_insert (s : set α) (T : set (set α)) : ⋃₀ (insert s T) = s ∪ ⋃₀ T := Sup_insert @@ -942,41 +935,15 @@ lemma bUnion_Union (s : ι → set α) (t : α → set β) : (⋃ x ∈ ⋃ i, s i, t x) = ⋃ i (x ∈ s i), t x := by simp [@Union_comm _ ι] -/-- If `S` is a set of sets, and each `s ∈ S` can be represented as an intersection -of sets `T s hs`, then `⋂₀ S` is the intersection of the union of all `T s hs`. -/ -lemma sInter_bUnion {S : set (set α)} {T : Π s ∈ S, set (set α)} - (hT : ∀ s ∈ S, s = ⋂₀ T s ‹s ∈ S›) : - ⋂₀ (⋃ s ∈ S, T s ‹_›) = ⋂₀ S := -begin - ext, - simp only [and_imp, exists_prop, set.mem_sInter, set.mem_Union, exists_imp_distrib], - split, - { rintro H s sS, - rw [hT s sS, mem_sInter], - exact λ t, H t s sS }, - { rintro H t s sS tTs, - suffices : s ⊆ t, exact this (H s sS), - rw [hT s sS, sInter_eq_bInter], - exact bInter_subset_of_mem tTs } -end +lemma bInter_Union (s : ι → set α) (t : α → set β) : + (⋂ x ∈ ⋃ i, s i, t x) = ⋂ i (x ∈ s i), t x := +by simp [@Inter_comm _ ι] -/-- If `S` is a set of sets, and each `s ∈ S` can be represented as an union -of sets `T s hs`, then `⋃₀ S` is the union of the union of all `T s hs`. -/ -lemma sUnion_bUnion {S : set (set α)} {T : Π s ∈ S, set (set α)} (hT : ∀ s ∈ S, s = ⋃₀ T s ‹_›) : - ⋃₀ (⋃ s ∈ S, T s ‹_›) = ⋃₀ S := -begin - ext, - simp only [exists_prop, set.mem_Union, set.mem_set_of_eq], - split, - { rintro ⟨t, ⟨s, sS, tTs⟩, xt⟩, - refine ⟨s, sS, _⟩, - rw hT s sS, - exact subset_sUnion_of_mem tTs xt }, - { rintro ⟨s, sS, xs⟩, - rw hT s sS at xs, - rcases mem_sUnion.1 xs with ⟨t, tTs, xt⟩, - exact ⟨t, ⟨s, sS, tTs⟩, xt⟩ } -end +lemma sUnion_Union (s : ι → set (set α)) : ⋃₀ (⋃ i, s i) = ⋃ i, ⋃₀ (s i) := +by simp only [sUnion_eq_bUnion, bUnion_Union] + +theorem sInter_Union (s : ι → set (set α)) : ⋂₀ (⋃ i, s i) = ⋂ i, ⋂₀ s i := +by simp only [sInter_eq_bInter, bInter_Union] lemma Union_range_eq_sUnion {α β : Type*} (C : set (set α)) {f : ∀ (s : C), β → s} (hf : ∀ (s : C), surjective (f s)) : diff --git a/src/order/bounded_order.lean b/src/order/bounded_order.lean index fd8f1807c2291..505e2987609f0 100644 --- a/src/order/bounded_order.lean +++ b/src/order/bounded_order.lean @@ -959,6 +959,9 @@ by { intro h, rw [←h, disjoint_self] at hab, exact ha hab } lemma disjoint.eq_bot_of_le {a b : α} (hab : disjoint a b) (h : a ≤ b) : a = ⊥ := eq_bot_iff.2 (by rwa ←inf_eq_left.2 h) +lemma disjoint_assoc {a b c : α} : disjoint (a ⊓ b) c ↔ disjoint a (b ⊓ c) := +by rw [disjoint, disjoint, inf_assoc] + lemma disjoint.of_disjoint_inf_of_le {a b c : α} (h : disjoint (a ⊓ b) c) (hle : a ≤ c) : disjoint a b := by rw [disjoint_iff, h.eq_bot_of_le (inf_le_left.trans hle)] diff --git a/src/order/filter/basic.lean b/src/order/filter/basic.lean index 1e1516e2cc7b2..0aa2f88e41683 100644 --- a/src/order/filter/basic.lean +++ b/src/order/filter/basic.lean @@ -825,14 +825,14 @@ lemma is_compl_principal (s : set α) : is_compl (𝓟 s) (𝓟 sᶜ) := ⟨by simp only [inf_principal, inter_compl_self, principal_empty, le_refl], by simp only [sup_principal, union_compl_self, principal_univ, le_refl]⟩ +theorem mem_inf_principal' {f : filter α} {s t : set α} : + s ∈ f ⊓ 𝓟 t ↔ tᶜ ∪ s ∈ f := +by simp only [← le_principal_iff, (is_compl_principal s).le_left_iff, disjoint_assoc, inf_principal, + ← (is_compl_principal (t ∩ sᶜ)).le_right_iff, compl_inter, compl_compl] + theorem mem_inf_principal {f : filter α} {s t : set α} : s ∈ f ⊓ 𝓟 t ↔ {x | x ∈ t → x ∈ s} ∈ f := -begin - simp only [← le_principal_iff, (is_compl_principal s).le_left_iff, disjoint, inf_assoc, - inf_principal, imp_iff_not_or], - rw [← disjoint, ← (is_compl_principal (t ∩ sᶜ)).le_right_iff, compl_inter, compl_compl], - refl -end +by { simp only [mem_inf_principal', imp_iff_not_or], refl } lemma supr_inf_principal (f : ι → filter α) (s : set α) : (⨆ i, f i ⊓ 𝓟 s) = (⨆ i, f i) ⊓ 𝓟 s := diff --git a/src/order/filter/countable_Inter.lean b/src/order/filter/countable_Inter.lean index 126b8994933c0..56d6ad89c2494 100644 --- a/src/order/filter/countable_Inter.lean +++ b/src/order/filter/countable_Inter.lean @@ -101,6 +101,23 @@ lemma eventually_eq.countable_bInter {S : set ι} (hS : countable S) {s t : Π i (eventually_le.countable_bInter hS (λ i hi, (h i hi).le)).antisymm (eventually_le.countable_bInter hS (λ i hi, (h i hi).symm.le)) +/-- Construct a filter with countable intersection property. This constructor deduces +`filter.univ_sets` and `filter.inter_sets` from the countable intersection property. -/ +def filter.of_countable_Inter (l : set (set α)) + (hp : ∀ S : set (set α), countable S → S ⊆ l → (⋂₀ S) ∈ l) + (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) : + filter α := +{ sets := l, + univ_sets := @sInter_empty α ▸ hp _ countable_empty (empty_subset _), + sets_of_superset := h_mono, + inter_sets := λ s t hs ht, sInter_pair s t ▸ + hp _ ((countable_singleton _).insert _) (insert_subset.2 ⟨hs, singleton_subset_iff.2 ht⟩) } + +instance filter.countable_Inter_of_countable_Inter (l : set (set α)) + (hp : ∀ S : set (set α), countable S → S ⊆ l → (⋂₀ S) ∈ l) + (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) : + countable_Inter_filter (filter.of_countable_Inter l hp h_mono) := ⟨hp⟩ + instance countable_Inter_filter_principal (s : set α) : countable_Inter_filter (𝓟 s) := ⟨λ S hSc hS, subset_sInter hS⟩ diff --git a/src/topology/bases.lean b/src/topology/bases.lean index d1d7eff584a0b..0af7b4aa0cdde 100644 --- a/src/topology/bases.lean +++ b/src/topology/bases.lean @@ -592,8 +592,8 @@ 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. -/ +/-- 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 := diff --git a/src/topology/lindelof.lean b/src/topology/lindelof.lean new file mode 100644 index 0000000000000..07c125403cfca --- /dev/null +++ b/src/topology/lindelof.lean @@ -0,0 +1,283 @@ +/- +Copyright (c) 2022 Yury Kudryashov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yury Kudryashov +-/ +import topology.bases +import order.filter.countable_Inter +import tactic.tfae + +/-! +-/ + +open filter set topological_space +open_locale filter topological_space + +variables {ι X Y : Type*} [topological_space X] [topological_space Y] {s t : set X} + +def is_lindelof (s : set X) : Prop := +∀ ⦃U : set (set X)⦄, (∀ u ∈ U, is_open u) → (s ⊆ ⋃₀ U) → ∃ V ⊆ U, countable V ∧ s ⊆ ⋃₀ V + +lemma is_lindelof.countable_open_subcover (h : is_lindelof s) {U : ι → set X} + (hU : ∀ i, is_open (U i)) (hsU : s ⊆ ⋃ i, U i) : + ∃ I : set ι, countable I ∧ s ⊆ ⋃ i ∈ I, U i := +begin + rcases @h (range U) (forall_range_iff.2 hU) hsU with ⟨V, hVU, hVc, hsV⟩, + haveI := hVc.to_encodable, + choose i hi using λ v : V, @hVU v v.2, + refine ⟨range i, countable_range _, _⟩, + simpa only [bUnion_range, hi, ← sUnion_eq_Union] +end + +lemma is_lindelof.countable_open_subcover₂ (h : is_lindelof s) {t : set ι} (U : Π i ∈ t, set X) + (hU : ∀ i ∈ t, is_open (U i ‹_›)) (hsU : s ⊆ ⋃ i ∈ t, U i ‹i ∈ t›) : + ∃ I ⊆ t, countable I ∧ s ⊆ ⋃ i ∈ I, U i (‹I ⊆ t› ‹i ∈ I›) := +begin + rw bUnion_eq_Union at hsU, + rcases h.countable_open_subcover (λ i : t, hU i i.2) hsU with ⟨I, hIc, hsI⟩, + refine ⟨coe '' I, subtype.coe_image_subset _ _, hIc.image _, _⟩, + simpa [Union_coe_set] using hsI +end + +lemma is_lindelof_of_exists_cluster_pt + (h : ∀ (f : filter X) [ne_bot f] [countable_Inter_filter f], s ∈ f → ∃ a ∈ s, cluster_pt a f) : + is_lindelof s := +begin + intros U hUo hsU, + set p : set X → Prop := λ u, ∃ I ⊆ U, countable I ∧ s \ u ⊆ ⋃₀ I, + have hp : ∀ S : set (set X), countable S → (∀ u ∈ S, p u) → p (⋂₀ S), + { intros S hSc hS, + choose! I hIU hIc hI using hS, + refine ⟨⋃ u ∈ S, I u, Union₂_subset hIU, hSc.bUnion hIc, _⟩, + simp only [bUnion_Union, sInter_eq_bInter, diff_Inter, sUnion_Union], + exact Union₂_mono hI }, + have hp_mono : ∀ u v, p u → u ⊆ v → p v, + { rintro u v ⟨I, hIU, hIc, hsub⟩ huv, + exact ⟨I, hIU, hIc, (diff_subset_diff_right huv).trans hsub⟩ }, + set f : filter X := filter.of_countable_Inter {u | p u} hp hp_mono, + have hf : ∀ {u}, u ∈ f ↔ p u := λ _, iff.rfl, + suffices : ¬ne_bot f, + { simp_rw [ne_bot_iff, not_not, ← empty_mem_iff_bot, hf, p, diff_empty] at this, + exact this }, + introI hfne, + have : s ∈ f, + { refine ⟨∅, empty_subset _, countable_empty, _⟩, + rw diff_self, exact empty_subset _ }, + rcases h _ this with ⟨x, hxs, hxf⟩, + rcases hsU hxs with ⟨t, htU, hxt⟩, + have : s \ t ∈ f, + { refine ⟨{t}, singleton_subset_iff.2 htU, countable_singleton t, _⟩, + rw [sdiff_sdiff_right_self, sUnion_singleton], + exact inter_subset_right _ _ }, + rcases cluster_pt_iff.1 hxf ((hUo t htU).mem_nhds hxt) this with ⟨y, hy, -, hy'⟩, + exact hy' hy +end + +/-- A list of properties of a set that are equivalent to `is_lindelof`. Use one of +`is_lindelof_iff_*` or `is_lindelof.*` lemmas instead. -/ +lemma is_lindelof_tfae (s : set X) : + tfae [is_lindelof s, + ∀ t : X → set X, (∀ x ∈ s, t x ∈ 𝓝 x) → ∃ I ⊆ s, countable I ∧ s ⊆ ⋃ x ∈ I, t x, + ∀ t : X → set X, (∀ x ∈ s, t x ∈ 𝓝[s] x) → ∃ I ⊆ s, countable I ∧ s ⊆ ⋃ x ∈ I, t x, + ∀ U : X → set X, (∀ x, is_open (U x)) → (∀ x, x ∈ U x) → + ∃ I ⊆ s, countable I ∧ s ⊆ ⋃ x ∈ I, U x, + ∀ T : set (set X), (∀ x ∈ s, ∃ t ∈ T, t ∈ 𝓝 x) → ∃ I ⊆ T, countable I ∧ s ⊆ ⋃₀ I, + ∀ T : set (set X), (∀ x ∈ s, ∃ t ∈ T, t ∈ 𝓝[s] x) → ∃ I ⊆ T, countable I ∧ s ⊆ ⋃₀ I, + ∀ ⦃f⦄ [ne_bot f] [countable_Inter_filter f], s ∈ f → ∃ a ∈ s, cluster_pt a f] := +begin + tfae_have : 1 → 3, + { intros H t ht, + simp only [mem_nhds_within] at ht, + choose u huo hxu hut using ht, + rcases H.countable_open_subcover₂ _ huo (λ x hx, mem_Union₂.2 ⟨x, hx, hxu x hx⟩) + with ⟨I, hIs, hIc, hsI⟩, + replace hsI := subset_inter hsI subset.rfl, rw Union₂_inter at hsI, + exact ⟨I, hIs, hIc, hsI.trans $ Union₂_mono $ λ x hx, hut x _⟩ }, + tfae_have : 3 → 2, from λ H t ht, H t (λ x hx, mem_nhds_within_of_mem_nhds (ht x hx)), + tfae_have : 2 → 4, + from λ H U hUo hU, H U (λ x hx, (hUo x).mem_nhds (hU x)), + tfae_have : 4 → 6, + { intros H T hT, + simp only [(nhds_within_basis_open _ _).mem_iff] at hT, + replace hT : ∀ x ∈ s, ∃ (u : {u : set X // x ∈ u ∧ is_open u}) (t ∈ T), ↑u ∩ s ⊆ t, + by simpa only [subtype.exists', @exists_swap {t // t ∈ T}] using hT, + haveI : ∀ x, nonempty {u : set X // x ∈ u ∧ is_open u} := λ x, ⟨⟨univ, trivial, is_open_univ⟩⟩, + choose! u t htT ht using hT, + rcases H (λ x, u x) (λ x, (u x).2.2) (λ x, (u x).2.1) with ⟨I, hIs, hIc, hsI⟩, + refine ⟨t '' I, image_subset_iff.2 (λ x hx, htT _ $ hIs hx), hIc.image _, λ x hx, _⟩, + rcases mem_Union₂.1 (hsI hx) with ⟨i, hi, hxi⟩, + exact ⟨t i, mem_image_of_mem t hi, ht i (hIs hi) ⟨hxi, hx⟩⟩ }, + tfae_have : 6 → 5, + { intros H T hT, + exact H T (λ x hx, (hT x hx).imp $ λ t ht, ⟨ht.fst, mem_nhds_within_of_mem_nhds ht.snd⟩) }, + tfae_have : 5 → 1, + { refine λ H U hUo hsU, H U (λ x hx, _), + rcases hsU hx with ⟨t, ht, hxt⟩, + exact ⟨t, ht, (hUo _ ht).mem_nhds hxt⟩ }, + tfae_have : 7 → 1, from is_lindelof_of_exists_cluster_pt, + tfae_have : 2 → 7, + { introsI H f hne hfI hsf, + simp only [cluster_pt_iff, ← not_disjoint_iff_nonempty_inter], + by_contra h, push_neg at h, + choose! t ht V hV hd using h, + rcases H t ht with ⟨I, hIs, hIc, hsI⟩, + have : (⋃ x ∈ I, t x) ∩ (⋂ x ∈ I, V x) ∈ f, + from inter_mem (mem_of_superset hsf hsI) + ((countable_bInter_mem hIc).2 $ λ x hx, hV _ (hIs hx)), + rcases filter.nonempty_of_mem this with ⟨x, hxt, hxV⟩, + rw mem_Inter₂ at hxV, rw mem_Union₂ at hxt, rcases hxt with ⟨i, hi, hxi⟩, + exact @hd i (hIs hi) x ⟨hxi, hxV _ hi⟩}, + tfae_finish +end + +lemma is_lindelof_iff_countable_cover_nhds : is_lindelof s ↔ + ∀ {t : X → set X}, (∀ x ∈ s, t x ∈ 𝓝 x) → ∃ I ⊆ s, countable I ∧ s ⊆ ⋃ x ∈ I, t x := +(is_lindelof_tfae s).out 0 1 + +alias is_lindelof_iff_countable_cover_nhds ↔ is_lindelof.countable_cover_nhds _ + +lemma is_lindelof_iff_countable_cover_nhds_within : is_lindelof s ↔ + ∀ {t : X → set X}, (∀ x ∈ s, t x ∈ 𝓝[s] x) → ∃ I ⊆ s, countable I ∧ s ⊆ ⋃ x ∈ I, t x := +(is_lindelof_tfae s).out 0 2 + +alias is_lindelof_iff_countable_cover_nhds_within ↔ is_lindelof.countable_cover_nhds_within _ + +lemma is_lindelof_iff_countable_cover_open_nhds : is_lindelof s ↔ + ∀ {u : X → set X}, (∀ x, is_open (u x)) → (∀ x, x ∈ u x) → + ∃ I ⊆ s, countable I ∧ s ⊆ ⋃ x ∈ I, u x := +(is_lindelof_tfae s).out 0 3 + +alias is_lindelof_iff_countable_cover_open_nhds ↔ is_lindelof.countable_cover_open_nhds _ + +lemma is_lindelof_iff_countable_sUnion_nhds : is_lindelof s ↔ + ∀ {T : set (set X)}, (∀ x ∈ s, ∃ t ∈ T, t ∈ 𝓝 x) → ∃ I ⊆ T, countable I ∧ s ⊆ ⋃₀ I := +(is_lindelof_tfae s).out 0 4 + +alias is_lindelof_iff_countable_sUnion_nhds ↔ is_lindelof.countable_sUnion_nhds _ + +lemma is_lindelof_iff_countable_sUnion_nhds_within : is_lindelof s ↔ + ∀ {T : set (set X)}, (∀ x ∈ s, ∃ t ∈ T, t ∈ 𝓝[s] x) → ∃ I ⊆ T, countable I ∧ s ⊆ ⋃₀ I := +(is_lindelof_tfae s).out 0 5 + +alias is_lindelof_iff_countable_sUnion_nhds_within ↔ is_lindelof.countable_sUnion_nhds_within _ + +lemma is_lindelof_iff_exists_cluster_pt : is_lindelof s ↔ + ∀ (f : filter X) [ne_bot f] [countable_Inter_filter f], s ∈ f → ∃ a ∈ s, cluster_pt a f := +(is_lindelof_tfae s).out 0 6 + +lemma is_lindelof.exists_cluster_pt {f : filter X} [ne_bot f] [countable_Inter_filter f] + (hs : is_lindelof s) (hsf : s ∈ f) : ∃ a ∈ s, cluster_pt a f := +is_lindelof_iff_exists_cluster_pt.mp hs f hsf + +lemma is_lindelof_Union [encodable ι] {s : ι → set X} (h : ∀ i, is_lindelof (s i)) : + is_lindelof (⋃ i, s i) := +begin + intros U hUo hsU, + choose V hVU hVc hsV using λ i, (h i) hUo (Union_subset_iff.1 hsU i), + refine ⟨⋃ i, V i, Union_subset hVU, countable_Union hVc, _⟩, + simpa only [sUnion_Union] using Union_mono hsV +end + +lemma is_lindelof_bUnion {I : set ι} (hI : countable I) {s : Π i ∈ I, set X} + (hs : ∀ i ∈ I, is_lindelof (s i ‹i ∈ I›)) : is_lindelof (⋃ i ∈ I, s i ‹i ∈ I›) := +begin + haveI := hI.to_encodable, + simp only [set_coe.forall', bUnion_eq_Union] at hs ⊢, + exact is_lindelof_Union hs +end + +protected lemma set.countable.is_lindelof (hs : countable s) : is_lindelof s := +is_lindelof_iff_countable_cover_nhds.mpr $ λ t ht, + ⟨s, subset.rfl, hs, λ x hx, mem_Union₂.2 ⟨x, hx, mem_of_mem_nhds (ht x hx)⟩⟩ + +protected lemma set.finite.is_lindelof (hs : finite s) : is_lindelof s := +hs.countable.is_lindelof + +protected lemma set.subsingleton.is_lindelof (hs : s.subsingleton) : is_lindelof s := +hs.finite.is_lindelof + +@[simp] lemma is_lindelof_empty : is_lindelof (∅ : set X) := +countable_empty.is_lindelof + +@[simp] lemma is_lindelof_singleton (x : X) : is_lindelof ({x} : set X) := +(countable_singleton x).is_lindelof + +lemma is_lindelof.inter_closed (hs : is_lindelof s) (ht : is_closed t) : + is_lindelof (s ∩ t) := +begin + apply is_lindelof_of_exists_cluster_pt, introsI f h₁ h₂ hstf, + rw inter_mem_iff at hstf, + obtain ⟨a, hsa, ha⟩ : ∃ a ∈ s, cluster_pt a f, from hs.exists_cluster_pt hstf.1, + have : a ∈ t := + (ht.mem_of_nhds_within_ne_bot $ ha.mono $ le_principal_iff.2 hstf.2), + exact ⟨a, ⟨hsa, this⟩, ha⟩ +end + +lemma is_closed.inter_lindelof (hs : is_closed s) (ht : is_lindelof t) : is_lindelof (s ∩ t) := +inter_comm t s ▸ ht.inter_closed hs + +lemma is_lindelof.subset (hs : is_lindelof s) (hts : t ⊆ s) (ht : is_closed t) : is_lindelof t := +by simpa only [inter_eq_self_of_subset_right hts] using hs.inter_closed ht + +lemma is_lindelof.image_of_continuous_on (hs : is_lindelof s) {f : X → Y} (hf : continuous_on f s) : + is_lindelof (f '' s) := +begin + refine is_lindelof_iff_countable_cover_nhds_within.mpr (λ t ht, _), + have : ∀ x ∈ s, f ⁻¹' (t (f x)) ∈ 𝓝[s] x, + from λ x hx, (hf x hx).tendsto_nhds_within_image (ht (f x) (mem_image_of_mem f hx)), + rcases hs.countable_cover_nhds_within this with ⟨I, hIs, hIc, hI⟩, + refine ⟨f '' I, image_subset _ hIs, hIc.image f, _⟩, + simpa +end + +lemma is_lindelof.image (hs : is_lindelof s) {f : X → Y} (hf : continuous f) : + is_lindelof (f '' s) := +hs.image_of_continuous_on hf.continuous_on + +lemma inducing.is_lindelof_image {e : X → Y} (he : inducing e) : + is_lindelof (e '' s) ↔ is_lindelof s := +begin + refine ⟨λ h, _, λ h, h.image he.continuous⟩, + refine is_lindelof_iff_countable_cover_open_nhds.mpr (λ u huo hxu, _), + replace huo := λ x, he.is_open_iff.1 (huo x), -- `simp only ... at huo` fails + choose v hvo hv using huo, obtain rfl : (λ x, e ⁻¹' (v x)) = u := funext hv, + have : e '' s ⊆ ⋃ x ∈ s, v x, + from image_subset_iff.2 (λ x hx, mem_Union₂.2 ⟨x, hx, hxu x⟩), + simpa using h.countable_open_subcover₂ _ (λ x _, hvo x) this +end + +lemma embedding.is_lindelof_image {e : X → Y} (he : embedding e) : + is_lindelof (e '' s) ↔ is_lindelof s := +he.to_inducing.is_lindelof_image + +class lindelof_space (X : Type*) [topological_space X] : Prop := +(is_lindelof_univ : is_lindelof (univ : set X)) + +export lindelof_space (is_lindelof_univ) + +lemma is_lindelof_univ_iff : is_lindelof (univ : set X) ↔ lindelof_space X := ⟨λ h, ⟨h⟩, λ h, h.1⟩ + +protected lemma is_closed.is_lindelof [lindelof_space X] {s : set X} (hs : is_closed s) : + is_lindelof s := +is_lindelof_univ.subset (subset_univ s) hs + +lemma is_lindelof_iff_lindelof_space : is_lindelof s ↔ lindelof_space s := +by rw [← is_lindelof_univ_iff, ← embedding_subtype_coe.is_lindelof_image, image_univ, + subtype.range_coe] + +alias is_lindelof_iff_lindelof_space ↔ is_lindelof.to_subtype _ + +@[protect_proj] +class strongly_lindelof_space (X : Type*) [topological_space X] : Prop := +(is_lindelof : ∀ s : set X, is_lindelof s) + +protected lemma set.is_lindelof [strongly_lindelof_space X] (s : set X) : is_lindelof s := +strongly_lindelof_space.is_lindelof s + +instance second_countable_topology.to_strongly_lindelof_space + [second_countable_topology X] : strongly_lindelof_space X := +begin + refine ⟨λ s U hUo hU, _⟩, + rcases is_open_sUnion_countable U hUo with ⟨S, hSc, hSU, hS⟩, + exact ⟨S, hSU, hSc, hS.symm ▸ hU⟩ +end diff --git a/src/topology/metric_space/baire.lean b/src/topology/metric_space/baire.lean index 8e2349429a981..49cd1032122d1 100644 --- a/src/topology/metric_space/baire.lean +++ b/src/topology/metric_space/baire.lean @@ -171,17 +171,17 @@ theorem dense_sInter_of_Gδ {S : set (set α)} (ho : ∀s∈S, is_Gδ s) (hS : c begin -- the result follows from the result for a countable intersection of dense open sets, -- by rewriting each set as a countable intersection of open sets, which are of course dense. - choose T hT using ho, - have : ⋂₀ S = ⋂₀ (⋃s∈S, T s ‹_›) := (sInter_bUnion (λs hs, (hT s hs).2.2)).symm, + choose T hTo hTc hsT using ho, + have : ⋂₀ S = ⋂₀ (⋃ s ∈ S, T s ‹_›), -- := (sInter_bUnion (λs hs, (hT s hs).2.2)).symm, + by simp only [sInter_Union, (hsT _ _).symm, ← sInter_eq_bInter], rw this, - refine dense_sInter_of_open _ (hS.bUnion (λs hs, (hT s hs).2.1)) _; - simp only [set.mem_Union, exists_prop]; rintro t ⟨s, hs, tTs⟩, - show is_open t, - { exact (hT s hs).1 t tTs }, + refine dense_sInter_of_open _ (hS.bUnion hTc) _; + simp only [mem_Union]; rintro t ⟨s, hs, tTs⟩, + show is_open t, from hTo s hs t tTs, show dense t, { intro x, have := hd s hs x, - rw (hT s hs).2.2 at this, + rw hsT s hs at this, exact closure_mono (sInter_subset_of_mem tTs) this } end From a763de51660d6c425af7c38424b5c03bf0a44b11 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 26 Jan 2022 11:46:24 -0500 Subject: [PATCH 02/15] feat(order/filter/countable_Inter): review - drop `_sets` in more names; - add `filter.of_countable_Inter` and instances for `filter.map`/`filter.comap`; - add docs. --- src/order/filter/countable_Inter.lean | 67 +++++++++++++++++++++++---- 1 file changed, 58 insertions(+), 9 deletions(-) diff --git a/src/order/filter/countable_Inter.lean b/src/order/filter/countable_Inter.lean index 126b8994933c0..48c7dc690b176 100644 --- a/src/order/filter/countable_Inter.lean +++ b/src/order/filter/countable_Inter.lean @@ -14,42 +14,50 @@ property: for any countable collection of sets `s ∈ l` their intersection belo Two main examples are the `residual` filter defined in `topology.metric_space.baire` and the `measure.ae` filter defined in `measure_theory.measure_space`. + +We reformulate the definition in terms of indexed intersection and in terms of `filter.eventually` +and provide instances for some basic constructions (`⊥`, `⊤`, `filter.principal`, `filter.map`, +`filter.comap`, `has_inf.inf`). We also provide a custom constructor `filter.of_countable_Inter` +that deduces two axioms of a `filter` from the countable intersection property. + +## Tags +filter, countable -/ open set filter open_locale filter -variables {ι α : Type*} +variables {ι α β : Type*} /-- A filter `l` has the countable intersection property if for any countable collection of sets `s ∈ l` their intersection belongs to `l` as well. -/ class countable_Inter_filter (l : filter α) : Prop := -(countable_sInter_mem_sets' : +(countable_sInter_mem' : ∀ {S : set (set α)} (hSc : countable S) (hS : ∀ s ∈ S, s ∈ l), ⋂₀ S ∈ l) variables {l : filter α} [countable_Inter_filter l] -lemma countable_sInter_mem_sets {S : set (set α)} (hSc : countable S) : +lemma countable_sInter_mem {S : set (set α)} (hSc : countable S) : ⋂₀ S ∈ l ↔ ∀ s ∈ S, s ∈ l := ⟨λ hS s hs, mem_of_superset hS (sInter_subset_of_mem hs), - countable_Inter_filter.countable_sInter_mem_sets' hSc⟩ + countable_Inter_filter.countable_sInter_mem' hSc⟩ -lemma countable_Inter_mem_sets [encodable ι] {s : ι → set α} : +lemma countable_Inter_mem [encodable ι] {s : ι → set α} : (⋂ i, s i) ∈ l ↔ ∀ i, s i ∈ l := -sInter_range s ▸ (countable_sInter_mem_sets (countable_range _)).trans forall_range_iff +sInter_range s ▸ (countable_sInter_mem (countable_range _)).trans forall_range_iff lemma countable_bInter_mem {S : set ι} (hS : countable S) {s : Π i ∈ S, set α} : (⋂ i ∈ S, s i ‹_›) ∈ l ↔ ∀ i ∈ S, s i ‹_› ∈ l := begin rw [bInter_eq_Inter], haveI := hS.to_encodable, - exact countable_Inter_mem_sets.trans subtype.forall + exact countable_Inter_mem.trans subtype.forall end lemma eventually_countable_forall [encodable ι] {p : α → ι → Prop} : (∀ᶠ x in l, ∀ i, p x i) ↔ ∀ i, ∀ᶠ x in l, p x i := by simpa only [filter.eventually, set_of_forall] - using @countable_Inter_mem_sets _ _ l _ _ (λ i, {x | p x i}) + using @countable_Inter_mem _ _ l _ _ (λ i, {x | p x i}) lemma eventually_countable_ball {S : set ι} (hS : countable S) {p : Π (x : α) (i ∈ S), Prop} : (∀ᶠ x in l, ∀ i ∈ S, p x i ‹_›) ↔ ∀ i ∈ S, ∀ᶠ x in l, p x i ‹_› := @@ -101,6 +109,29 @@ lemma eventually_eq.countable_bInter {S : set ι} (hS : countable S) {s t : Π i (eventually_le.countable_bInter hS (λ i hi, (h i hi).le)).antisymm (eventually_le.countable_bInter hS (λ i hi, (h i hi).symm.le)) +/-- Construct a filter with countable intersection property. This constructor deduces +`filter.univ_sets` and `filter.inter_sets` from the countable intersection property. -/ +def filter.of_countable_Inter (l : set (set α)) + (hp : ∀ S : set (set α), countable S → S ⊆ l → (⋂₀ S) ∈ l) + (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) : + filter α := +{ sets := l, + univ_sets := @sInter_empty α ▸ hp _ countable_empty (empty_subset _), + sets_of_superset := h_mono, + inter_sets := λ s t hs ht, sInter_pair s t ▸ + hp _ ((countable_singleton _).insert _) (insert_subset.2 ⟨hs, singleton_subset_iff.2 ht⟩) } + +instance filter.countable_Inter_of_countable_Inter (l : set (set α)) + (hp : ∀ S : set (set α), countable S → S ⊆ l → (⋂₀ S) ∈ l) + (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) : + countable_Inter_filter (filter.of_countable_Inter l hp h_mono) := ⟨hp⟩ + +@[simp] lemma filter.mem_of_countable_Inter {l : set (set α)} + (hp : ∀ S : set (set α), countable S → S ⊆ l → (⋂₀ S) ∈ l) + (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) {s : set α} : + s ∈ filter.of_countable_Inter l hp h_mono ↔ s ∈ l := +iff.rfl + instance countable_Inter_filter_principal (s : set α) : countable_Inter_filter (𝓟 s) := ⟨λ S hSc hS, subset_sInter hS⟩ @@ -110,6 +141,24 @@ by { rw ← principal_empty, apply countable_Inter_filter_principal } instance countable_Inter_filter_top : countable_Inter_filter (⊤ : filter α) := by { rw ← principal_univ, apply countable_Inter_filter_principal } +instance (l : filter β) [countable_Inter_filter l] (f : α → β) : + countable_Inter_filter (comap f l) := +begin + refine ⟨λ S hSc hS, _⟩, + choose! t htl ht using hS, + have : (⋂ s ∈ S, t s) ∈ l, from (countable_bInter_mem hSc).2 htl, + refine ⟨_, this, _⟩, + simpa [preimage_Inter] using (Inter₂_mono ht) +end + +instance (l : filter α) [countable_Inter_filter l] (f : α → β) : + countable_Inter_filter (map f l) := +begin + constructor, intros S hSc hS, + simp only [mem_map, sInter_eq_bInter, preimage_Inter₂] at hS ⊢, + exact (countable_bInter_mem hSc).2 hS +end + /-- Infimum of two `countable_Inter_filter`s is a `countable_Inter_filter`. This is useful, e.g., to automatically get an instance for `residual α ⊓ 𝓟 s`. -/ instance countable_Inter_filter_inf (l₁ l₂ : filter α) [countable_Inter_filter l₁] @@ -130,6 +179,6 @@ instance countable_Inter_filter_sup (l₁ l₂ : filter α) [countable_Inter_fil [countable_Inter_filter l₂] : countable_Inter_filter (l₁ ⊔ l₂) := begin - refine ⟨λ S hSc hS, ⟨_, _⟩⟩; refine (countable_sInter_mem_sets hSc).2 (λ s hs, _), + refine ⟨λ S hSc hS, ⟨_, _⟩⟩; refine (countable_sInter_mem hSc).2 (λ s hs, _), exacts [(hS s hs).1, (hS s hs).2] end From 38c8b7a4c7a47d7db1e8bc61019d226a0cc92d66 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 26 Jan 2022 11:48:41 -0500 Subject: [PATCH 03/15] Snapshot --- src/data/set/lattice.lean | 59 ++++++---------------------- src/topology/metric_space/baire.lean | 14 +++---- 2 files changed, 20 insertions(+), 53 deletions(-) diff --git a/src/data/set/lattice.lean b/src/data/set/lattice.lean index e38d60bc8fa3d..8b25751161b9b 100644 --- a/src/data/set/lattice.lean +++ b/src/data/set/lattice.lean @@ -67,7 +67,7 @@ instance : has_Sup (set α) := ⟨sUnion⟩ /-- Intersection of a set of sets. -/ def sInter (S : set (set α)) : set α := Inf S -prefix `⋂₀`:110 := sInter +prefix `⋂₀ `:110 := sInter @[simp] theorem mem_sInter {x : α} {S : set (set α)} : x ∈ ⋂₀ S ↔ ∀ t ∈ S, x ∈ t := iff.rfl @@ -701,12 +701,12 @@ theorem bUnion_union (s t : set α) (u : α → set β) : (⋃ x ∈ s ∪ t, u x) = (⋃ x ∈ s, u x) ∪ (⋃ x ∈ t, u x) := supr_union -@[simp] lemma Union_coe_set {α β : Type*} (s : set α) (f : α → set β) : - (⋃ (i : s), f i) = ⋃ (i ∈ s), f i := +@[simp] lemma Union_coe_set {α β : Type*} (s : set α) (f : s → set β) : + (⋃ i, f i) = ⋃ i ∈ s, f ⟨i, ‹i ∈ s›⟩ := Union_subtype _ _ -@[simp] lemma Inter_coe_set {α β : Type*} (s : set α) (f : α → set β) : - (⋂ (i : s), f i) = ⋂ (i ∈ s), f i := +@[simp] lemma Inter_coe_set {α β : Type*} (s : set α) (f : s → set β) : + (⋂ i, f i) = ⋂ i ∈ s, f ⟨i, ‹i ∈ s›⟩ := Inter_subtype _ _ theorem bUnion_insert (a : α) (s : set α) (t : α → set β) : @@ -785,13 +785,6 @@ theorem sUnion_union (S T : set (set α)) : ⋃₀ (S ∪ T) = ⋃₀ S ∪ ⋃ theorem sInter_union (S T : set (set α)) : ⋂₀ (S ∪ T) = ⋂₀ S ∩ ⋂₀ T := Inf_union -theorem sInter_Union (s : ι → set (set α)) : ⋂₀ (⋃ i, s i) = ⋂ i, ⋂₀ s i := -begin - ext x, - simp only [mem_Union, mem_Inter, mem_sInter, exists_imp_distrib], - split; tauto -end - @[simp] theorem sUnion_insert (s : set α) (T : set (set α)) : ⋃₀ (insert s T) = s ∪ ⋃₀ T := Sup_insert @@ -942,41 +935,15 @@ lemma bUnion_Union (s : ι → set α) (t : α → set β) : (⋃ x ∈ ⋃ i, s i, t x) = ⋃ i (x ∈ s i), t x := by simp [@Union_comm _ ι] -/-- If `S` is a set of sets, and each `s ∈ S` can be represented as an intersection -of sets `T s hs`, then `⋂₀ S` is the intersection of the union of all `T s hs`. -/ -lemma sInter_bUnion {S : set (set α)} {T : Π s ∈ S, set (set α)} - (hT : ∀ s ∈ S, s = ⋂₀ T s ‹s ∈ S›) : - ⋂₀ (⋃ s ∈ S, T s ‹_›) = ⋂₀ S := -begin - ext, - simp only [and_imp, exists_prop, set.mem_sInter, set.mem_Union, exists_imp_distrib], - split, - { rintro H s sS, - rw [hT s sS, mem_sInter], - exact λ t, H t s sS }, - { rintro H t s sS tTs, - suffices : s ⊆ t, exact this (H s sS), - rw [hT s sS, sInter_eq_bInter], - exact bInter_subset_of_mem tTs } -end +lemma bInter_Union (s : ι → set α) (t : α → set β) : + (⋂ x ∈ ⋃ i, s i, t x) = ⋂ i (x ∈ s i), t x := +by simp [@Inter_comm _ ι] -/-- If `S` is a set of sets, and each `s ∈ S` can be represented as an union -of sets `T s hs`, then `⋃₀ S` is the union of the union of all `T s hs`. -/ -lemma sUnion_bUnion {S : set (set α)} {T : Π s ∈ S, set (set α)} (hT : ∀ s ∈ S, s = ⋃₀ T s ‹_›) : - ⋃₀ (⋃ s ∈ S, T s ‹_›) = ⋃₀ S := -begin - ext, - simp only [exists_prop, set.mem_Union, set.mem_set_of_eq], - split, - { rintro ⟨t, ⟨s, sS, tTs⟩, xt⟩, - refine ⟨s, sS, _⟩, - rw hT s sS, - exact subset_sUnion_of_mem tTs xt }, - { rintro ⟨s, sS, xs⟩, - rw hT s sS at xs, - rcases mem_sUnion.1 xs with ⟨t, tTs, xt⟩, - exact ⟨t, ⟨s, sS, tTs⟩, xt⟩ } -end +lemma sUnion_Union (s : ι → set (set α)) : ⋃₀ (⋃ i, s i) = ⋃ i, ⋃₀ (s i) := +by simp only [sUnion_eq_bUnion, bUnion_Union] + +theorem sInter_Union (s : ι → set (set α)) : ⋂₀ (⋃ i, s i) = ⋂ i, ⋂₀ s i := +by simp only [sInter_eq_bInter, bInter_Union] lemma Union_range_eq_sUnion {α β : Type*} (C : set (set α)) {f : ∀ (s : C), β → s} (hf : ∀ (s : C), surjective (f s)) : diff --git a/src/topology/metric_space/baire.lean b/src/topology/metric_space/baire.lean index 8e2349429a981..49cd1032122d1 100644 --- a/src/topology/metric_space/baire.lean +++ b/src/topology/metric_space/baire.lean @@ -171,17 +171,17 @@ theorem dense_sInter_of_Gδ {S : set (set α)} (ho : ∀s∈S, is_Gδ s) (hS : c begin -- the result follows from the result for a countable intersection of dense open sets, -- by rewriting each set as a countable intersection of open sets, which are of course dense. - choose T hT using ho, - have : ⋂₀ S = ⋂₀ (⋃s∈S, T s ‹_›) := (sInter_bUnion (λs hs, (hT s hs).2.2)).symm, + choose T hTo hTc hsT using ho, + have : ⋂₀ S = ⋂₀ (⋃ s ∈ S, T s ‹_›), -- := (sInter_bUnion (λs hs, (hT s hs).2.2)).symm, + by simp only [sInter_Union, (hsT _ _).symm, ← sInter_eq_bInter], rw this, - refine dense_sInter_of_open _ (hS.bUnion (λs hs, (hT s hs).2.1)) _; - simp only [set.mem_Union, exists_prop]; rintro t ⟨s, hs, tTs⟩, - show is_open t, - { exact (hT s hs).1 t tTs }, + refine dense_sInter_of_open _ (hS.bUnion hTc) _; + simp only [mem_Union]; rintro t ⟨s, hs, tTs⟩, + show is_open t, from hTo s hs t tTs, show dense t, { intro x, have := hd s hs x, - rw (hT s hs).2.2 at this, + rw hsT s hs at this, exact closure_mono (sInter_subset_of_mem tTs) this } end From 37e98d464d67fa338274320ead09090a36caca19 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 26 Jan 2022 13:18:35 -0500 Subject: [PATCH 04/15] Fix --- src/order/filter/basic.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/order/filter/basic.lean b/src/order/filter/basic.lean index 1e1516e2cc7b2..ac1390148bb03 100644 --- a/src/order/filter/basic.lean +++ b/src/order/filter/basic.lean @@ -524,7 +524,8 @@ begin refine ⟨I, If, λ i, if hi : i ∈ I then V ⟨i, hi⟩ else univ, λ i, _, λ i hi, _, _⟩, { split_ifs, exacts [hV _, univ_mem] }, { exact dif_neg hi }, - { simp [Inter_dite, bInter_eq_Inter] } + { simp only [Inter_dite, bInter_eq_Inter, dif_pos (subtype.coe_prop _), subtype.coe_eta, + Inter_univ, inter_univ, eq_self_iff_true, true_and] } end lemma exists_Inter_of_mem_infi {ι : Type*} {α : Type*} {f : ι → filter α} {s} From 579fb50531c190cc0782c5685bd1002d09c09c0a Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 26 Jan 2022 14:09:37 -0500 Subject: [PATCH 05/15] Fix --- src/topology/paracompact.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/topology/paracompact.lean b/src/topology/paracompact.lean index 99ff863b45c9f..5484ec7d20727 100644 --- a/src/topology/paracompact.lean +++ b/src/topology/paracompact.lean @@ -113,7 +113,7 @@ begin have := hT, simp only [subset_def, mem_Union] at this, choose i hiT hi using λ x, this x (mem_univ x), refine ⟨(T : set ι), λ t, s t, λ t, ho _, _, locally_finite_of_fintype _, λ t, ⟨t, subset.rfl⟩⟩, - rwa [Union_coe_set, finset.set_bUnion_coe, ← univ_subset_iff], + simpa only [Union_coe_set, ← univ_subset_iff] end /-- Let `X` be a locally compact sigma compact Hausdorff topological space, let `s` be a closed set From 93e6f8787968e43e5866e4c8fe75cb6ce671ea1d Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 26 Jan 2022 16:32:01 -0500 Subject: [PATCH 06/15] Revert --- src/order/filter/basic.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/order/filter/basic.lean b/src/order/filter/basic.lean index d90dcc399fbf5..6bcd3670d1137 100644 --- a/src/order/filter/basic.lean +++ b/src/order/filter/basic.lean @@ -839,14 +839,14 @@ lemma is_compl_principal (s : set α) : is_compl (𝓟 s) (𝓟 sᶜ) := ⟨by simp only [inf_principal, inter_compl_self, principal_empty, le_refl], by simp only [sup_principal, union_compl_self, principal_univ, le_refl]⟩ -theorem mem_inf_principal' {f : filter α} {s t : set α} : - s ∈ f ⊓ 𝓟 t ↔ tᶜ ∪ s ∈ f := -by simp only [← le_principal_iff, (is_compl_principal s).le_left_iff, disjoint_assoc, inf_principal, - ← (is_compl_principal (t ∩ sᶜ)).le_right_iff, compl_inter, compl_compl] - theorem mem_inf_principal {f : filter α} {s t : set α} : s ∈ f ⊓ 𝓟 t ↔ {x | x ∈ t → x ∈ s} ∈ f := -by { simp only [mem_inf_principal', imp_iff_not_or], refl } +begin + simp only [← le_principal_iff, (is_compl_principal s).le_left_iff, disjoint, inf_assoc, + inf_principal, imp_iff_not_or], + rw [← disjoint, ← (is_compl_principal (t ∩ sᶜ)).le_right_iff, compl_inter, compl_compl], + refl +end lemma supr_inf_principal (f : ι → filter α) (s : set α) : (⨆ i, f i ⊓ 𝓟 s) = (⨆ i, f i) ⊓ 𝓟 s := From 550b39dbf29b110a281d6a8b4059d20c531121d6 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 26 Jan 2022 16:34:51 -0500 Subject: [PATCH 07/15] Revert --- src/order/bounded_order.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/order/bounded_order.lean b/src/order/bounded_order.lean index 505e2987609f0..fd8f1807c2291 100644 --- a/src/order/bounded_order.lean +++ b/src/order/bounded_order.lean @@ -959,9 +959,6 @@ by { intro h, rw [←h, disjoint_self] at hab, exact ha hab } lemma disjoint.eq_bot_of_le {a b : α} (hab : disjoint a b) (h : a ≤ b) : a = ⊥ := eq_bot_iff.2 (by rwa ←inf_eq_left.2 h) -lemma disjoint_assoc {a b c : α} : disjoint (a ⊓ b) c ↔ disjoint a (b ⊓ c) := -by rw [disjoint, disjoint, inf_assoc] - lemma disjoint.of_disjoint_inf_of_le {a b c : α} (h : disjoint (a ⊓ b) c) (hle : a ≤ c) : disjoint a b := by rw [disjoint_iff, h.eq_bot_of_le (inf_le_left.trans hle)] From d2ffced2c8559665ca1a1995b8e56cb8dd92698c Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 26 Jan 2022 17:11:56 -0500 Subject: [PATCH 08/15] Snapshot --- src/topology/lindelof.lean | 4 ++-- src/topology/subset_properties.lean | 32 ++++++++++++----------------- 2 files changed, 15 insertions(+), 21 deletions(-) diff --git a/src/topology/lindelof.lean b/src/topology/lindelof.lean index 07c125403cfca..bdcd9f138ef21 100644 --- a/src/topology/lindelof.lean +++ b/src/topology/lindelof.lean @@ -251,7 +251,7 @@ lemma embedding.is_lindelof_image {e : X → Y} (he : embedding e) : he.to_inducing.is_lindelof_image class lindelof_space (X : Type*) [topological_space X] : Prop := -(is_lindelof_univ : is_lindelof (univ : set X)) +(is_lindelof_univ [] : is_lindelof (univ : set X)) export lindelof_space (is_lindelof_univ) @@ -259,7 +259,7 @@ lemma is_lindelof_univ_iff : is_lindelof (univ : set X) ↔ lindelof_space X := protected lemma is_closed.is_lindelof [lindelof_space X] {s : set X} (hs : is_closed s) : is_lindelof s := -is_lindelof_univ.subset (subset_univ s) hs +(is_lindelof_univ X).subset (subset_univ s) hs lemma is_lindelof_iff_lindelof_space : is_lindelof s ↔ lindelof_space s := by rw [← is_lindelof_univ_iff, ← embedding_subtype_coe.is_lindelof_image, image_univ, diff --git a/src/topology/subset_properties.lean b/src/topology/subset_properties.lean index 619880591f573..8d23f56086c34 100644 --- a/src/topology/subset_properties.lean +++ b/src/topology/subset_properties.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov -/ import order.filter.pi -import topology.bases +import topology.lindelof import data.finset.order import data.set.accumulate import tactic.tfae @@ -60,6 +60,10 @@ section compact there exists `a ∈ s` such that every set of `f` meets every neighborhood of `a`. -/ def is_compact (s : set α) := ∀ ⦃f⦄ [ne_bot f], f ≤ 𝓟 s → ∃ a ∈ s, cluster_pt a f +/-- A compact set is a Lindelöf set. -/ +protected lemma is_compact.is_lindelof (h : is_compact s) : is_lindelof s := +is_lindelof_iff_exists_cluster_pt.mpr $ λ f hne _ hsf, @h f hne (le_principal_iff.2 hsf) + /-- The complement to a compact set belongs to a filter `f` if it belongs to each filter `𝓝 a ⊓ f`, `a ∈ s`. -/ lemma is_compact.compl_mem_sets (hs : is_compact s) {f : filter α} (hf : ∀ a ∈ s, sᶜ ∈ 𝓝 a ⊓ f) : @@ -1129,33 +1133,23 @@ protected noncomputable def locally_finite.encodable {ι : Type*} {f : ι → se (hf : locally_finite f) (hne : ∀ i, (f i).nonempty) : encodable ι := @encodable.of_equiv _ _ (hf.countable_univ hne).to_encodable (equiv.set.univ _).symm +@[priority 100] -- see Note [lower instance priority] +instance sigma_compact_space.lindelof_space [sigma_compact_space α] : lindelof_space α := +⟨Union_compact_covering α ▸ is_lindelof_Union $ λ k, (is_compact_compact_covering α k).is_lindelof⟩ + /-- In a topological space with sigma compact topology, if `f` is a function that sends each point `x` of a closed set `s` to a neighborhood of `x` within `s`, then for some countable set `t ⊆ s`, the neighborhoods `f x`, `x ∈ t`, cover the whole set `s`. -/ lemma countable_cover_nhds_within_of_sigma_compact {f : α → set α} {s : set α} (hs : is_closed s) (hf : ∀ x ∈ s, f x ∈ 𝓝[s] x) : ∃ t ⊆ s, countable t ∧ s ⊆ ⋃ x ∈ t, f x := -begin - simp only [nhds_within, mem_inf_principal] at hf, - choose t ht hsub using λ n, ((is_compact_compact_covering α n).inter_right hs).elim_nhds_subcover - _ (λ x hx, hf x hx.right), - refine ⟨⋃ n, (t n : set α), Union_subset $ λ n x hx, (ht n x hx).2, - countable_Union $ λ n, (t n).countable_to_set, λ x hx, mem_Union₂.2 _⟩, - rcases exists_mem_compact_covering x with ⟨n, hn⟩, - rcases mem_Union₂.1 (hsub n ⟨hn, hx⟩) with ⟨y, hyt : y ∈ t n, hyf : x ∈ s → x ∈ f y⟩, - exact ⟨y, mem_Union.2 ⟨n, hyt⟩, hyf hx⟩ -end +hs.is_lindelof.countable_cover_nhds_within hf /-- In a topological space with sigma compact 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_of_sigma_compact {f : α → set α} - (hf : ∀ x, f x ∈ 𝓝 x) : ∃ s : set α, countable s ∧ (⋃ x ∈ s, f x) = univ := -begin - simp only [← nhds_within_univ] at hf, - rcases countable_cover_nhds_within_of_sigma_compact is_closed_univ (λ x _, hf x) - with ⟨s, -, hsc, hsU⟩, - exact ⟨s, hsc, univ_subset_iff.1 hsU⟩ -end +lemma countable_cover_nhds_of_sigma_compact {f : α → set α} (hf : ∀ x, f x ∈ 𝓝 x) : + ∃ s : set α, countable s ∧ (⋃ x ∈ s, f x) = univ := +by simpa [univ_subset_iff] using (is_lindelof_univ α).countable_cover_nhds (λ x _, hf x) end compact From b1423d355ee8c381f0e4c862c6cdfa5e800065d2 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 26 Jan 2022 20:07:05 -0500 Subject: [PATCH 09/15] Snapshot --- src/topology/bases.lean | 39 +++++------------------- src/topology/lindelof.lean | 40 +++++++++++++++++++++++++ src/topology/subset_properties.lean | 46 +++++------------------------ 3 files changed, 55 insertions(+), 70 deletions(-) diff --git a/src/topology/bases.lean b/src/topology/bases.lean index 0af7b4aa0cdde..1b09eb8ec5c0c 100644 --- a/src/topology/bases.lean +++ b/src/topology/bases.lean @@ -21,19 +21,19 @@ 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. -* `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.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 @@ -615,29 +615,6 @@ let ⟨T, cT, hT⟩ := is_open_Union_countable (λ s:S, s.1) (λ s, H s.1 s.2) i 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 - end topological_space open topological_space diff --git a/src/topology/lindelof.lean b/src/topology/lindelof.lean index bdcd9f138ef21..656fc1902817c 100644 --- a/src/topology/lindelof.lean +++ b/src/topology/lindelof.lean @@ -250,6 +250,18 @@ lemma embedding.is_lindelof_image {e : X → Y} (he : embedding e) : is_lindelof (e '' s) ↔ is_lindelof s := he.to_inducing.is_lindelof_image +lemma locally_finite.countable_nonempty_inter_lindelof {f : ι → set X} (hf : locally_finite f) + (hs : is_lindelof s) : + countable {i : ι | (f i ∩ s).nonempty} := +begin + choose U hxU hUf using hf, + rcases hs.countable_cover_nhds (λ x _, hxU x) with ⟨I, hIs, hIc, hsI⟩, + refine (hIc.bUnion $ λ x _, (hUf x).countable).mono _, + rintro i ⟨x, hi, hxs⟩, + rcases mem_Union₂.1 (hsI hxs) with ⟨y, hyI, hxy⟩, + exact mem_Union₂.2 ⟨y, hyI, ⟨x, hi, hxy⟩⟩ +end + class lindelof_space (X : Type*) [topological_space X] : Prop := (is_lindelof_univ [] : is_lindelof (univ : set X)) @@ -267,6 +279,26 @@ by rw [← is_lindelof_univ_iff, ← embedding_subtype_coe.is_lindelof_image, im alias is_lindelof_iff_lindelof_space ↔ is_lindelof.to_subtype _ +/-- In a Lindelöf topological space, 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 [lindelof_space X] {f : X → set X} + (hf : ∀ x, f x ∈ 𝓝 x) : ∃ s : set X, countable s ∧ (⋃ x ∈ s, f x) = univ := +by simpa [univ_subset_iff] using (is_lindelof_univ X).countable_cover_nhds (λ x _, hf x) + +/-- If `α` is a `σ`-compact space, then a locally finite family of nonempty sets of `α` can have +only countably many elements, `set.countable` version. -/ +protected lemma locally_finite.countable_univ [lindelof_space X] {f : ι → set X} + (hf : locally_finite f) (hne : ∀ i, (f i).nonempty) : + countable (univ : set ι) := +by simpa only [inter_univ, hne] using hf.countable_nonempty_inter_lindelof (is_lindelof_univ X) + +/-- If `f : ι → set α` is a locally finite covering of a Lindelöf topological space by nonempty +sets, then the index type `ι` is encodable. -/ +protected noncomputable def locally_finite.encodable [lindelof_space X] {f : ι → set X} + (hf : locally_finite f) (hne : ∀ i, (f i).nonempty) : encodable ι := +@encodable.of_equiv _ _ (hf.countable_univ hne).to_encodable (equiv.set.univ _).symm + @[protect_proj] class strongly_lindelof_space (X : Type*) [topological_space X] : Prop := (is_lindelof : ∀ s : set X, is_lindelof s) @@ -281,3 +313,11 @@ begin rcases is_open_sUnion_countable U hUo with ⟨S, hSc, hSU, hS⟩, exact ⟨S, hSU, hSc, hS.symm ▸ hU⟩ end + +lemma countable_cover_nhds_within [strongly_lindelof_space X] {f : X → set X} {s : set X} + (hf : ∀ x ∈ s, f x ∈ 𝓝[s] x) : ∃ t ⊆ s, countable t ∧ s ⊆ (⋃ x ∈ t, f x) := +s.is_lindelof.countable_cover_nhds_within hf + +@[priority 100] +instance strongly_lindelof_space.lindelof_space [strongly_lindelof_space X] : lindelof_space X := +⟨set.is_lindelof univ⟩ diff --git a/src/topology/subset_properties.lean b/src/topology/subset_properties.lean index 8d23f56086c34..d039190f34071 100644 --- a/src/topology/subset_properties.lean +++ b/src/topology/subset_properties.lean @@ -1080,8 +1080,8 @@ lemma sigma_compact_space.of_countable (S : set (set α)) (Hc : countable S) ⟨(exists_seq_cover_iff_countable ⟨_, is_compact_empty⟩).2 ⟨S, Hc, Hcomp, HU⟩⟩ @[priority 100] -- see Note [lower instance priority] -instance sigma_compact_space_of_locally_compact_second_countable [locally_compact_space α] - [second_countable_topology α] : sigma_compact_space α := +instance sigma_compact_space_of_locally_compact_lindelof [locally_compact_space α] + [lindelof_space α] : sigma_compact_space α := begin choose K hKc hxK using λ x : α, exists_compact_mem_nhds x, rcases countable_cover_nhds hxK with ⟨s, hsc, hsU⟩, @@ -1109,48 +1109,16 @@ end compact_covering α m ⊆ compact_covering α n := monotone_accumulate h +/-- A `σ`-compact topological space is a Lindelöf space. This is not an instance to avoid a loop +with `sigma_compact_space_of_locally_compact_lindelof`. -/ +lemma sigma_compact_space.lindelof_space [sigma_compact_space α] : lindelof_space α := +⟨Union_compact_covering α ▸ is_lindelof_Union $ λ k, (is_compact_compact_covering α k).is_lindelof⟩ + variable {α} lemma exists_mem_compact_covering (x : α) : ∃ n, x ∈ compact_covering α n := Union_eq_univ_iff.mp (Union_compact_covering α) x -/-- If `α` is a `σ`-compact space, then a locally finite family of nonempty sets of `α` can have -only countably many elements, `set.countable` version. -/ -protected lemma locally_finite.countable_univ {ι : Type*} {f : ι → set α} (hf : locally_finite f) - (hne : ∀ i, (f i).nonempty) : - countable (univ : set ι) := -begin - have := λ n, hf.finite_nonempty_inter_compact (is_compact_compact_covering α n), - refine (countable_Union (λ n, (this n).countable)).mono (λ i hi, _), - rcases hne i with ⟨x, hx⟩, - rcases Union_eq_univ_iff.1 (Union_compact_covering α) x with ⟨n, hn⟩, - exact mem_Union.2 ⟨n, x, hx, hn⟩ -end - -/-- If `f : ι → set α` is a locally finite covering of a σ-compact topological space by nonempty -sets, then the index type `ι` is encodable. -/ -protected noncomputable def locally_finite.encodable {ι : Type*} {f : ι → set α} - (hf : locally_finite f) (hne : ∀ i, (f i).nonempty) : encodable ι := -@encodable.of_equiv _ _ (hf.countable_univ hne).to_encodable (equiv.set.univ _).symm - -@[priority 100] -- see Note [lower instance priority] -instance sigma_compact_space.lindelof_space [sigma_compact_space α] : lindelof_space α := -⟨Union_compact_covering α ▸ is_lindelof_Union $ λ k, (is_compact_compact_covering α k).is_lindelof⟩ - -/-- In a topological space with sigma compact topology, if `f` is a function that sends each point -`x` of a closed set `s` to a neighborhood of `x` within `s`, then for some countable set `t ⊆ s`, -the neighborhoods `f x`, `x ∈ t`, cover the whole set `s`. -/ -lemma countable_cover_nhds_within_of_sigma_compact {f : α → set α} {s : set α} (hs : is_closed s) - (hf : ∀ x ∈ s, f x ∈ 𝓝[s] x) : ∃ t ⊆ s, countable t ∧ s ⊆ ⋃ x ∈ t, f x := -hs.is_lindelof.countable_cover_nhds_within hf - -/-- In a topological space with sigma compact 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_of_sigma_compact {f : α → set α} (hf : ∀ x, f x ∈ 𝓝 x) : - ∃ s : set α, countable s ∧ (⋃ x ∈ s, f x) = univ := -by simpa [univ_subset_iff] using (is_lindelof_univ α).countable_cover_nhds (λ x _, hf x) - end compact /-- An [exhaustion by compact sets](https://en.wikipedia.org/wiki/Exhaustion_by_compact_sets) of a From 25f56ce1d7919210c26bf121b13e2ab67e0be6b4 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sat, 29 Jan 2022 03:51:07 -0500 Subject: [PATCH 10/15] Snapshot --- src/geometry/manifold/charted_space.lean | 41 ++++++----- src/geometry/manifold/partition_of_unity.lean | 6 +- .../smooth_manifold_with_corners.lean | 4 + src/measure_theory/measure/measure_space.lean | 7 +- src/measure_theory/measure/outer_measure.lean | 17 +++-- src/topology/bases.lean | 23 ------ src/topology/lindelof.lean | 73 +++++++++++++++---- src/topology/subset_properties.lean | 20 +++-- 8 files changed, 122 insertions(+), 69 deletions(-) diff --git a/src/geometry/manifold/charted_space.lean b/src/geometry/manifold/charted_space.lean index baa4940a1a64d..1e3adaef15429 100644 --- a/src/geometry/manifold/charted_space.lean +++ b/src/geometry/manifold/charted_space.lean @@ -497,6 +497,22 @@ 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 _ _) +open topological_space + +lemma charted_space.second_countable_of_countable_cover [second_countable_topology H] + {s : set M} (hs : (⋃ x (hx : x ∈ s), (chart_at H x).source) = univ) + (hsc : countable s) : + second_countable_topology M := +begin + haveI : ∀ x : M, second_countable_topology (chart_at H x).source := + λ x, (chart_at H x).second_countable_topology_source, + haveI := hsc.to_encodable, + rw bUnion_eq_Union at hs, + exact second_countable_topology_of_countable_cover (λ x : s, (chart_at H (x : M)).open_source) hs +end + +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 := @@ -513,28 +529,19 @@ begin exact h₂.image_of_continuous_on ((chart_at H x).continuous_on_symm.mono h₃) end -open topological_space - -lemma charted_space.second_countable_of_countable_cover [second_countable_topology H] - {s : set M} (hs : (⋃ x (hx : x ∈ s), (chart_at H x).source) = univ) - (hsc : countable s) : +lemma charted_space.second_countable_of_lindelof [second_countable_topology H] [lindelof_space M] : second_countable_topology M := begin - haveI : ∀ x : M, second_countable_topology (chart_at H x).source := - λ x, (chart_at H x).second_countable_topology_source, - haveI := hsc.to_encodable, - rw bUnion_eq_Union at hs, - exact second_countable_topology_of_countable_cover (λ x : s, (chart_at H (x : M)).open_source) hs + obtain ⟨s, hsc, hsU⟩ : ∃ s, countable s ∧ (⋃ x (hx : x ∈ s), (chart_at H x).source) = univ := + 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.second_countable_of_sigma_compact [second_countable_topology H] - [sigma_compact_space M] : - second_countable_topology M := +lemma charted_space.sigma_compact_of_lindelof [locally_compact_space H] [lindelof_space M] : + sigma_compact_space 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)), - exact charted_space.second_countable_of_countable_cover H hsU hsc + haveI := charted_space.locally_compact H M, + exact sigma_compact_space_of_locally_compact_lindelof M end end diff --git a/src/geometry/manifold/partition_of_unity.lean b/src/geometry/manifold/partition_of_unity.lean index 1c76468785d87..df3e407c58be9 100644 --- a/src/geometry/manifold/partition_of_unity.lean +++ b/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⟩, diff --git a/src/geometry/manifold/smooth_manifold_with_corners.lean b/src/geometry/manifold/smooth_manifold_with_corners.lean index c9420ce7121dd..b94c49489dd7a 100644 --- a/src/geometry/manifold/smooth_manifold_with_corners.lean +++ b/src/geometry/manifold/smooth_manifold_with_corners.lean @@ -261,6 +261,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 diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean index 1d06780135322..f8d06cfca5bbb 100644 --- a/src/measure_theory/measure/measure_space.lean +++ b/src/measure_theory/measure/measure_space.lean @@ -2431,9 +2431,14 @@ 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μ + /-- 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 diff --git a/src/measure_theory/measure/outer_measure.lean b/src/measure_theory/measure/outer_measure.lean index 6903ee3df348d..d3bd4aa7c53c0 100644 --- a/src/measure_theory/measure/outer_measure.lean +++ b/src/measure_theory/measure/outer_measure.lean @@ -111,19 +111,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) : diff --git a/src/topology/bases.lean b/src/topology/bases.lean index 1b09eb8ec5c0c..013a7b043f240 100644 --- a/src/topology/bases.lean +++ b/src/topology/bases.lean @@ -592,29 +592,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]⟩ - end topological_space open topological_space diff --git a/src/topology/lindelof.lean b/src/topology/lindelof.lean index 656fc1902817c..d2c7df397452b 100644 --- a/src/topology/lindelof.lean +++ b/src/topology/lindelof.lean @@ -29,7 +29,7 @@ begin simpa only [bUnion_range, hi, ← sUnion_eq_Union] end -lemma is_lindelof.countable_open_subcover₂ (h : is_lindelof s) {t : set ι} (U : Π i ∈ t, set X) +lemma is_lindelof.countable_open_subcover₂ (h : is_lindelof s) {t : set ι} {U : Π i ∈ t, set X} (hU : ∀ i ∈ t, is_open (U i ‹_›)) (hsU : s ⊆ ⋃ i ∈ t, U i ‹i ∈ t›) : ∃ I ⊆ t, countable I ∧ s ⊆ ⋃ i ∈ I, U i (‹I ⊆ t› ‹i ∈ I›) := begin @@ -89,7 +89,7 @@ begin { intros H t ht, simp only [mem_nhds_within] at ht, choose u huo hxu hut using ht, - rcases H.countable_open_subcover₂ _ huo (λ x hx, mem_Union₂.2 ⟨x, hx, hxu x hx⟩) + rcases H.countable_open_subcover₂ huo (λ x hx, mem_Union₂.2 ⟨x, hx, hxu x hx⟩) with ⟨I, hIs, hIc, hsI⟩, replace hsI := subset_inter hsI subset.rfl, rw Union₂_inter at hsI, exact ⟨I, hIs, hIc, hsI.trans $ Union₂_mono $ λ x hx, hut x _⟩ }, @@ -243,7 +243,7 @@ begin choose v hvo hv using huo, obtain rfl : (λ x, e ⁻¹' (v x)) = u := funext hv, have : e '' s ⊆ ⋃ x ∈ s, v x, from image_subset_iff.2 (λ x hx, mem_Union₂.2 ⟨x, hx, hxu x⟩), - simpa using h.countable_open_subcover₂ _ (λ x _, hvo x) this + simpa using h.countable_open_subcover₂ (λ x _, hvo x) this end lemma embedding.is_lindelof_image {e : X → Y} (he : embedding e) : @@ -273,12 +273,23 @@ protected lemma is_closed.is_lindelof [lindelof_space X] {s : set X} (hs : is_cl is_lindelof s := (is_lindelof_univ X).subset (subset_univ s) hs +lemma inducing.lindelof_space_iff {e : X → Y} (he : inducing e) : + lindelof_space X ↔ is_lindelof (range e) := +by rw [← is_lindelof_univ_iff, ← he.is_lindelof_image, image_univ] + +lemma embedding.lindelof_space_iff {e : X → Y} (he : embedding e) : + lindelof_space X ↔ is_lindelof (range e) := +he.to_inducing.lindelof_space_iff + lemma is_lindelof_iff_lindelof_space : is_lindelof s ↔ lindelof_space s := -by rw [← is_lindelof_univ_iff, ← embedding_subtype_coe.is_lindelof_image, image_univ, - subtype.range_coe] +by erw [embedding_subtype_coe.lindelof_space_iff, subtype.range_coe] alias is_lindelof_iff_lindelof_space ↔ is_lindelof.to_subtype _ +protected lemma closed_embedding.lindelof_space [lindelof_space Y] {e : X → Y} + (he : closed_embedding e) : lindelof_space X := +he.to_embedding.lindelof_space_iff.2 he.closed_range.is_lindelof + /-- In a Lindelöf topological space, 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. -/ @@ -299,21 +310,57 @@ protected noncomputable def locally_finite.encodable [lindelof_space X] {f : ι (hf : locally_finite f) (hne : ∀ i, (f i).nonempty) : encodable ι := @encodable.of_equiv _ _ (hf.countable_univ hne).to_encodable (equiv.set.univ _).symm -@[protect_proj] -class strongly_lindelof_space (X : Type*) [topological_space X] : Prop := -(is_lindelof : ∀ s : set X, is_lindelof s) +/-! +### Strongly (hereditarily) Lindelöf spaces -protected lemma set.is_lindelof [strongly_lindelof_space X] (s : set X) : is_lindelof s := -strongly_lindelof_space.is_lindelof s +A topological space is called *strongly (hereditarily) Lindelöf* if any set in this space is a +Lindelöf set. Any topological space with second countable topology is a strongly Lindelöf space. The +converse is not true. +-/ +class strongly_lindelof_space (X : Type*) [topological_space X] : Prop := +(is_lindelof_open : ∀ {s : set X}, is_open s → is_lindelof s) + +@[priority 100] instance second_countable_topology.to_strongly_lindelof_space [second_countable_topology X] : strongly_lindelof_space X := begin - refine ⟨λ s U hUo hU, _⟩, - rcases is_open_sUnion_countable U hUo with ⟨S, hSc, hSU, hS⟩, - exact ⟨S, hSU, hSc, hS.symm ▸ hU⟩ + refine ⟨λ s hs U hU hsU, _⟩, clear hs, + set B := {b ∈ countable_basis X | ∃ u ∈ U, b ⊆ u}, + choose! u huU hbu using (show ∀ b ∈ B, ∃ u ∈ U, b ⊆ u, from λ b, and.right), + refine ⟨u '' B, image_subset_iff.2 huU, + ((countable_countable_basis X).mono (sep_subset _ _)).image u, hsU.trans _⟩, + rintro x ⟨v, hvU, hxv⟩, + rcases (is_basis_countable_basis X).mem_nhds_iff.1 ((hU v hvU).mem_nhds hxv) + with ⟨b, hb, hxb, hbv⟩, + exact ⟨u b, mem_image_of_mem _ ⟨hb, v, hvU, hbv⟩, hbu _ ⟨hb, v, hvU, hbv⟩ hxb⟩ end +protected lemma set.is_lindelof [strongly_lindelof_space X] (s : set X) : is_lindelof s := +begin + intros U hU hsU, + have := strongly_lindelof_space.is_lindelof_open (is_open_sUnion hU), + rcases this.countable_open_subcover₂ hU sUnion_eq_bUnion.subset with ⟨V, hVU, hVc, hUV⟩, + simp only [← sUnion_eq_bUnion] at hUV, + exact ⟨V, hVU, hVc, hsU.trans hUV⟩ +end + +/-- In a strongly Lindelöf space (e.g., in a space with second countable topology), 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 [strongly_lindelof_space X] + (s : ι → set X) (H : ∀ i, is_open (s i)) : + ∃ T : set ι, countable T ∧ (⋃ i ∈ T, s i) = ⋃ i, s i := +let ⟨T, hTc, hT⟩ := (⋃ i, s i).is_lindelof.countable_open_subcover H subset.rfl +in ⟨T, hTc, (Union₂_subset_Union _ _).antisymm hT⟩ + +/-- In a strongly Lindelöf space (e.g., in a space with second countable topology), an open set, +given as a union of open sets, is equal to the union of countably many of those sets. -/ +lemma is_open_sUnion_countable [strongly_lindelof_space X] + (S : set (set X)) (H : ∀ s ∈ S, is_open s) : + ∃ T : set (set X), countable T ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S := +let ⟨T, hTS, hTc, hST⟩ := (⋃₀ S).is_lindelof.countable_open_subcover₂ H sUnion_eq_bUnion.subset +in ⟨T, hTc, hTS, (sUnion_mono hTS).antisymm (hST.trans sUnion_eq_bUnion.symm.subset)⟩ + lemma countable_cover_nhds_within [strongly_lindelof_space X] {f : X → set X} {s : set X} (hf : ∀ x ∈ s, f x ∈ 𝓝[s] x) : ∃ t ⊆ s, countable t ∧ s ⊆ (⋃ x ∈ t, f x) := s.is_lindelof.countable_cover_nhds_within hf diff --git a/src/topology/subset_properties.lean b/src/topology/subset_properties.lean index d039190f34071..2e78e7e31a9aa 100644 --- a/src/topology/subset_properties.lean +++ b/src/topology/subset_properties.lean @@ -1079,8 +1079,12 @@ lemma sigma_compact_space.of_countable (S : set (set α)) (Hc : countable S) (Hcomp : ∀ s ∈ S, is_compact s) (HU : ⋃₀ S = univ) : sigma_compact_space α := ⟨(exists_seq_cover_iff_countable ⟨_, is_compact_empty⟩).2 ⟨S, Hc, Hcomp, HU⟩⟩ -@[priority 100] -- see Note [lower instance priority] -instance sigma_compact_space_of_locally_compact_lindelof [locally_compact_space α] +variable (α) + +/-- A locally compact Lindelöf space is a σ-compact space. This is not an instance to avoid a loop +with `sigma_compact_space.lindelof_space`. A corollary of this lemma, +`sigma_compact_space_of_locally_compact_second_countable`, is registered as an instance. -/ +lemma sigma_compact_space_of_locally_compact_lindelof [locally_compact_space α] [lindelof_space α] : sigma_compact_space α := begin choose K hKc hxK using λ x : α, exists_compact_mem_nhds x, @@ -1089,7 +1093,12 @@ begin rwa sUnion_image end -variables (α) [sigma_compact_space α] +@[priority 100] -- see Note [lower instance priority] +instance sigma_compact_space_of_locally_compact_second_countable [locally_compact_space α] + [second_countable_topology α] : sigma_compact_space α := +sigma_compact_space_of_locally_compact_lindelof α + +variables [sigma_compact_space α] open sigma_compact_space /-- A choice of compact covering for a `σ`-compact space, chosen to be monotone. -/ @@ -1109,9 +1118,8 @@ end compact_covering α m ⊆ compact_covering α n := monotone_accumulate h -/-- A `σ`-compact topological space is a Lindelöf space. This is not an instance to avoid a loop -with `sigma_compact_space_of_locally_compact_lindelof`. -/ -lemma sigma_compact_space.lindelof_space [sigma_compact_space α] : lindelof_space α := +/-- A `σ`-compact topological space is a Lindelöf space. -/ +instance sigma_compact_space.lindelof_space [sigma_compact_space α] : lindelof_space α := ⟨Union_compact_covering α ▸ is_lindelof_Union $ λ k, (is_compact_compact_covering α k).is_lindelof⟩ variable {α} From a0cca9b1155a8b270c982ca3aa53655cf08a8beb Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sat, 29 Jan 2022 10:53:59 -0500 Subject: [PATCH 11/15] Snapshot --- src/measure_theory/measure/measure_space.lean | 4 +- .../metric_space/hausdorff_dimension.lean | 116 +++++++++++++----- 2 files changed, 84 insertions(+), 36 deletions(-) diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean index f8d06cfca5bbb..221608814c8cf 100644 --- a/src/measure_theory/measure/measure_space.lean +++ b/src/measure_theory/measure/measure_space.lean @@ -2411,11 +2411,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 diff --git a/src/topology/metric_space/hausdorff_dimension.lean b/src/topology/metric_space/hausdorff_dimension.lean index 871c872538040..8e0d89cfc779c 100644 --- a/src/topology/metric_space/hausdorff_dimension.lean +++ b/src/topology/metric_space/hausdorff_dimension.lean @@ -212,47 +212,67 @@ alias dimH_coe_finset ← finset.dimH_zero section -variables [second_countable_topology X] - -/-- If `r` is less than the Hausdorff dimension of a set `s` in an (extended) metric space with -second countable topology, then there exists a point `x ∈ s` such that every neighborhood -`t` of `x` within `s` has Hausdorff dimension greater than `r`. -/ -lemma exists_mem_nhds_within_lt_dimH_of_lt_dimH {s : set X} {r : ℝ≥0∞} (h : r < dimH s) : +/-- If `r` is less than the Hausdorff dimension of a Lindelöf set `s` in an (extended) metric space, +then there exists a point `x ∈ s` such that every neighborhood `t` of `x` within `s` has Hausdorff +dimension greater than `r`. -/ +lemma is_lindelof.exists_mem_nhds_within_lt_dimH_of_lt_dimH {s : set X} + (hs : is_lindelof s) {r : ℝ≥0∞} (h : r < dimH s) : ∃ x ∈ s, ∀ t ∈ 𝓝[s] x, r < dimH t := begin contrapose! h, choose! t htx htr using h, - rcases countable_cover_nhds_within htx with ⟨S, hSs, hSc, hSU⟩, + rcases hs.countable_cover_nhds_within htx with ⟨S, hSs, hSc, hSU⟩, calc dimH s ≤ dimH (⋃ x ∈ S, t x) : dimH_mono hSU ... = ⨆ x ∈ S, dimH (t x) : dimH_bUnion hSc _ ... ≤ r : bsupr_le (λ x hx, htr x (hSs hx)) end -/-- In an (extended) metric space with second countable topology, the Hausdorff dimension -of a set `s` is the supremum over `x ∈ s` of the limit superiors of `dimH t` along -`(𝓝[s] x).lift' powerset`. -/ -lemma bsupr_limsup_dimH (s : set X) : (⨆ x ∈ s, limsup ((𝓝[s] x).lift' powerset) dimH) = dimH s := +/-- If `r` is less than the Hausdorff dimension of a set `s` in an (extended) metric space with +second countable topology, then there exists a point `x ∈ s` such that every neighborhood +`t` of `x` within `s` has Hausdorff dimension greater than `r`. -/ +lemma exists_mem_nhds_within_lt_dimH_of_lt_dimH [second_countable_topology X] {s : set X} {r : ℝ≥0∞} + (h : r < dimH s) : ∃ x ∈ s, ∀ t ∈ 𝓝[s] x, r < dimH t := +s.is_lindelof.exists_mem_nhds_within_lt_dimH_of_lt_dimH h + +/-- In an (extended) metric space, the Hausdorff dimension of a Lindelöf set `s` is the supremum +over `x ∈ s` of the limit superiors of `dimH t` along `(𝓝[s] x).lift' powerset`. -/ +lemma is_lindelof.bsupr_limsup_dimH {s : set X} (hs : is_lindelof s) : + (⨆ x ∈ s, limsup ((𝓝[s] x).lift' powerset) dimH) = dimH s := begin refine le_antisymm (bsupr_le $ λ x hx, _) _, { refine Limsup_le_of_le (by apply_auto_param) (eventually_map.2 _), exact eventually_lift'_powerset.2 ⟨s, self_mem_nhds_within, λ t, dimH_mono⟩ }, { refine le_of_forall_ge_of_dense (λ r hr, _), - rcases exists_mem_nhds_within_lt_dimH_of_lt_dimH hr with ⟨x, hxs, hxr⟩, + rcases hs.exists_mem_nhds_within_lt_dimH_of_lt_dimH hr with ⟨x, hxs, hxr⟩, refine le_bsupr_of_le x hxs _, rw limsup_eq, refine le_Inf (λ b hb, _), rcases eventually_lift'_powerset.1 hb with ⟨t, htx, ht⟩, exact (hxr t htx).le.trans (ht t subset.rfl) } end /-- In an (extended) metric space with second countable topology, the Hausdorff dimension -of a set `s` is the supremum over all `x` of the limit superiors of `dimH t` along +of a set `s` is the supremum over `x ∈ s` of the limit superiors of `dimH t` along `(𝓝[s] x).lift' powerset`. -/ -lemma supr_limsup_dimH (s : set X) : (⨆ x, limsup ((𝓝[s] x).lift' powerset) dimH) = dimH s := +lemma bsupr_limsup_dimH [second_countable_topology X] (s : set X) : + (⨆ x ∈ s, limsup ((𝓝[s] x).lift' powerset) dimH) = dimH s := +s.is_lindelof.bsupr_limsup_dimH + +/-- In an (extended) metric space, the Hausdorff dimension of a Lindelöf set `s` is the supremum +over all `x` of the limit superiors of `dimH t` along `(𝓝[s] x).lift' powerset`. -/ +lemma is_lindelof.supr_limsup_dimH {s : set X} (hs : is_lindelof s) : + (⨆ x, limsup ((𝓝[s] x).lift' powerset) dimH) = dimH s := begin refine le_antisymm (supr_le $ λ x, _) _, { refine Limsup_le_of_le (by apply_auto_param) (eventually_map.2 _), exact eventually_lift'_powerset.2 ⟨s, self_mem_nhds_within, λ t, dimH_mono⟩ }, - { rw ← bsupr_limsup_dimH, exact bsupr_le_supr _ _ } + { rw ← hs.bsupr_limsup_dimH, exact bsupr_le_supr _ _ } end +/-- In an (extended) metric space with second countable topology, the Hausdorff dimension +of a set `s` is the supremum over all `x` of the limit superiors of `dimH t` along +`(𝓝[s] x).lift' powerset`. -/ +lemma supr_limsup_dimH [second_countable_topology X] (s : set X) : + (⨆ x, limsup ((𝓝[s] x).lift' powerset) dimH) = dimH s := +s.is_lindelof.supr_limsup_dimH + end /-! @@ -293,30 +313,45 @@ lemma dimH_range_le (h : holder_with C r f) (hr : 0 < r) : end holder_with -/-- If `s` is a set in a space `X` with second countable topology and `f : X → Y` is Hölder +/-- If `s` is a Lindelöf set in an (extended) metric space `X` and `f : X → Y` is Hölder continuous in a neighborhood within `s` of every point `x ∈ s` with the same positive exponent `r` but possibly different coefficients, then the Hausdorff dimension of the image `f '' s` is at most the Hausdorff dimension of `s` divided by `r`. -/ -lemma dimH_image_le_of_locally_holder_on [second_countable_topology X] {r : ℝ≥0} {f : X → Y} - (hr : 0 < r) {s : set X} (hf : ∀ x ∈ s, ∃ (C : ℝ≥0) (t ∈ 𝓝[s] x), holder_on_with C r f t) : +lemma is_lindelof.dimH_image_le_of_locally_holder_on {r : ℝ≥0} {f : X → Y} {s : set X} + (hs : is_lindelof s) (hr : 0 < r) + (hf : ∀ x ∈ s, ∃ (C : ℝ≥0) (t ∈ 𝓝[s] x), holder_on_with C r f t) : dimH (f '' s) ≤ dimH s / r := begin choose! C t htn hC using hf, - rcases countable_cover_nhds_within htn with ⟨u, hus, huc, huU⟩, + rcases hs.countable_cover_nhds_within htn with ⟨u, hus, huc, huU⟩, replace huU := inter_eq_self_of_subset_left huU, rw inter_Union₂ at huU, rw [← huU, image_Union₂, dimH_bUnion huc, dimH_bUnion huc], simp only [ennreal.supr_div], exact bsupr_le_bsupr (λ x hx, ((hC x (hus hx)).mono (inter_subset_right _ _)).dimH_image_le hr) end -/-- If `f : X → Y` is Hölder continuous in a neighborhood of every point `x : X` with the same -positive exponent `r` but possibly different coefficients, then the Hausdorff dimension of the range -of `f` is at most the Hausdorff dimension of `X` divided by `r`. -/ -lemma dimH_range_le_of_locally_holder_on [second_countable_topology X] {r : ℝ≥0} {f : X → Y} +/-- If `s` is a set in a space `X` with second countable topology and `f : X → Y` is Hölder +continuous in a neighborhood within `s` of every point `x ∈ s` with the same positive exponent `r` +but possibly different coefficients, then the Hausdorff dimension of the image `f '' s` is at most +the Hausdorff dimension of `s` divided by `r`. -/ +lemma dimH_image_le_of_locally_holder_on [second_countable_topology X] {r : ℝ≥0} {f : X → Y} + (hr : 0 < r) {s : set X} (hf : ∀ x ∈ s, ∃ (C : ℝ≥0) (t ∈ 𝓝[s] x), holder_on_with C r f t) : + dimH (f '' s) ≤ dimH s / r := +s.is_lindelof.dimH_image_le_of_locally_holder_on hr hf + +/-- If `f : X → Y` is Hölder continuous in a neighborhood of every point `x : X` of a second +countable (extended) metric space with the same positive exponent `r` but possibly different +coefficients, then the Hausdorff dimension of the range of `f` is at most the Hausdorff dimension of +`X` divided by `r`. + +We assume that `X` is a Lindelöf space instead of a space with second countable topology. While +these assumptions are equivalent, in this case lemma applies without an extra `haveI` whenever +one has either `[topological_space.second_countable_topology X]` or `[sigma_compact_space X]`. -/ +lemma dimH_range_le_of_locally_holder_on [lindelof_space X] {r : ℝ≥0} {f : X → Y} (hr : 0 < r) (hf : ∀ x : X, ∃ (C : ℝ≥0) (s ∈ 𝓝 x), holder_on_with C r f s) : dimH (range f) ≤ dimH (univ : set X) / r := begin rw ← image_univ, - refine dimH_image_le_of_locally_holder_on hr (λ x _, _), + refine (is_lindelof_univ X).dimH_image_le_of_locally_holder_on hr (λ x _, _), simpa only [exists_prop, nhds_within_univ] using hf x end @@ -341,27 +376,40 @@ lemma dimH_range_le (h : lipschitz_with K f) : dimH (range f) ≤ dimH (univ : s end lipschitz_with -/-- If `s` is a set in an extended metric space `X` with second countable topology and `f : X → Y` -is Lipschitz in a neighborhood within `s` of every point `x ∈ s`, then the Hausdorff dimension of -the image `f '' s` is at most the Hausdorff dimension of `s`. -/ -lemma dimH_image_le_of_locally_lipschitz_on [second_countable_topology X] {f : X → Y} - {s : set X} (hf : ∀ x ∈ s, ∃ (C : ℝ≥0) (t ∈ 𝓝[s] x), lipschitz_on_with C f t) : +/-- If `s` is a Lindelöf set in an extended metric space `X` and `f : X → Y` is Lipschitz in a +neighborhood within `s` of every point `x ∈ s`, then the Hausdorff dimension of the image `f '' s` +is at most the Hausdorff dimension of `s`. -/ +lemma is_lindelof.dimH_image_le_of_locally_lipschitz_on {f : X → Y} {s : set X} (hs : is_lindelof s) + (hf : ∀ x ∈ s, ∃ (C : ℝ≥0) (t ∈ 𝓝[s] x), lipschitz_on_with C f t) : dimH (f '' s) ≤ dimH s := begin have : ∀ x ∈ s, ∃ (C : ℝ≥0) (t ∈ 𝓝[s] x), holder_on_with C 1 f t, by simpa only [holder_on_with_one] using hf, simpa only [ennreal.coe_one, ennreal.div_one] - using dimH_image_le_of_locally_holder_on zero_lt_one this + using hs.dimH_image_le_of_locally_holder_on zero_lt_one this end -/-- If `f : X → Y` is Lipschitz in a neighborhood of each point `x : X`, then the Hausdorff -dimension of `range f` is at most the Hausdorff dimension of `X`. -/ -lemma dimH_range_le_of_locally_lipschitz_on [second_countable_topology X] {f : X → Y} +/-- If `s` is a set in an extended metric space `X` with second countable topology and `f : X → Y` +is Lipschitz in a neighborhood within `s` of every point `x ∈ s`, then the Hausdorff dimension of +the image `f '' s` is at most the Hausdorff dimension of `s`. -/ +lemma dimH_image_le_of_locally_lipschitz_on [second_countable_topology X] {f : X → Y} + {s : set X} (hf : ∀ x ∈ s, ∃ (C : ℝ≥0) (t ∈ 𝓝[s] x), lipschitz_on_with C f t) : + dimH (f '' s) ≤ dimH s := +s.is_lindelof.dimH_image_le_of_locally_lipschitz_on hf + +/-- If `f : X → Y` is Lipschitz in a neighborhood of each point `x : X` of an extended metric space +with second countable topology, then the Hausdorff dimension of `range f` is at most the Hausdorff +dimension of `X`. + +We assume that `X` is a Lindelöf space instead of a space with second countable topology. While +these assumptions are equivalent, in this case lemma applies without an extra `haveI` whenever +one has either `[topological_space.second_countable_topology X]` or `[sigma_compact_space X]`. -/ +lemma dimH_range_le_of_locally_lipschitz_on [lindelof_space X] {f : X → Y} (hf : ∀ x : X, ∃ (C : ℝ≥0) (s ∈ 𝓝 x), lipschitz_on_with C f s) : dimH (range f) ≤ dimH (univ : set X) := begin rw ← image_univ, - refine dimH_image_le_of_locally_lipschitz_on (λ x _, _), + refine (is_lindelof_univ X).dimH_image_le_of_locally_lipschitz_on (λ x _, _), simpa only [exists_prop, nhds_within_univ] using hf x end From fe91e6976c25b3de6c16405f871a0f7ed09fdeba Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 2 Feb 2022 00:03:14 -0500 Subject: [PATCH 12/15] Add docs, lower instance priority --- src/topology/lindelof.lean | 45 ++++++++++++++++++++++++++--- src/topology/subset_properties.lean | 1 + 2 files changed, 42 insertions(+), 4 deletions(-) diff --git a/src/topology/lindelof.lean b/src/topology/lindelof.lean index d2c7df397452b..a0d02130bd9fe 100644 --- a/src/topology/lindelof.lean +++ b/src/topology/lindelof.lean @@ -8,6 +8,25 @@ import order.filter.countable_Inter import tactic.tfae /-! +# Lindelöf sets and spaces + +In this file we define Lindelöf sets, Lindelöf spaces, and strongly (hereditarily) Lindelöf +spaces. We also prove that a topological space with second countable topology is a strongly Lindelöf +space. + +## Main definitions + +* We say that a set `s` in a topological space is a *Lindelöf set* if any open cover of `s` admits a + countable subcover. + +* A topological space `X` is said to be *Lindelöf* if the whole space is a Lindelöf set. + +* A topological space `X` is said to be *strongly (hereditarily) Lindelöf* if any set in `X` is a + Lindelöf set. + +## Tags + +Lindelöf space, open cover -/ open filter set topological_space @@ -15,6 +34,8 @@ open_locale filter topological_space variables {ι X Y : Type*} [topological_space X] [topological_space Y] {s t : set X} +/-- A set `s` in a topological space is called a *Lindelöf set* if any open cover of `s` admits a +countable subcover. -/ def is_lindelof (s : set X) : Prop := ∀ ⦃U : set (set X)⦄, (∀ u ∈ U, is_open u) → (s ⊆ ⋃₀ U) → ∃ V ⊆ U, countable V ∧ s ⊆ ⋃₀ V @@ -219,6 +240,8 @@ inter_comm t s ▸ ht.inter_closed hs lemma is_lindelof.subset (hs : is_lindelof s) (hts : t ⊆ s) (ht : is_closed t) : is_lindelof t := by simpa only [inter_eq_self_of_subset_right hts] using hs.inter_closed ht +/-- The image of a Lindelöf set under a function continuous on this set is a Lindelöf set. See also +`is_lindelof.image`. -/ lemma is_lindelof.image_of_continuous_on (hs : is_lindelof s) {f : X → Y} (hf : continuous_on f s) : is_lindelof (f '' s) := begin @@ -230,6 +253,8 @@ begin simpa end +/-- The image of a Lindelöf set under a continuous map is a Lindelöf set. See also +`is_lindelof.image_of_continuous_on`. -/ lemma is_lindelof.image (hs : is_lindelof s) {f : X → Y} (hf : continuous f) : is_lindelof (f '' s) := hs.image_of_continuous_on hf.continuous_on @@ -262,6 +287,8 @@ begin exact mem_Union₂.2 ⟨y, hyI, ⟨x, hi, hxy⟩⟩ end +/-- A topological space `X` is said to be a *Lindelöf space* if any open cover of `X` admits a +countable subcover. -/ class lindelof_space (X : Type*) [topological_space X] : Prop := (is_lindelof_univ [] : is_lindelof (univ : set X)) @@ -269,6 +296,7 @@ export lindelof_space (is_lindelof_univ) lemma is_lindelof_univ_iff : is_lindelof (univ : set X) ↔ lindelof_space X := ⟨λ h, ⟨h⟩, λ h, h.1⟩ +/-- A closed set in a Lindelöf space is a Lindelöf set. -/ protected lemma is_closed.is_lindelof [lindelof_space X] {s : set X} (hs : is_closed s) : is_lindelof s := (is_lindelof_univ X).subset (subset_univ s) hs @@ -281,6 +309,7 @@ lemma embedding.lindelof_space_iff {e : X → Y} (he : embedding e) : lindelof_space X ↔ is_lindelof (range e) := he.to_inducing.lindelof_space_iff +/-- A set is a Lindelöf set if and only if it is a Lindelöf space in the induced topology. -/ lemma is_lindelof_iff_lindelof_space : is_lindelof s ↔ lindelof_space s := by erw [embedding_subtype_coe.lindelof_space_iff, subtype.range_coe] @@ -318,6 +347,9 @@ Lindelöf set. Any topological space with second countable topology is a strongl converse is not true. -/ +/-- A topological space is called *strongly (hereditarily) Lindelöf* if any set in this space is a +Lindelöf set. We only require that open sets are Lindelöf in the definition, then deduce that any +set in a strongly Lindelöf space is Lindelöf in `set.is_lindelof`. -/ class strongly_lindelof_space (X : Type*) [topological_space X] : Prop := (is_lindelof_open : ∀ {s : set X}, is_open s → is_lindelof s) @@ -336,6 +368,7 @@ begin exact ⟨u b, mem_image_of_mem _ ⟨hb, v, hvU, hbv⟩, hbu _ ⟨hb, v, hvU, hbv⟩ hxb⟩ end +/-- Any set in a strongly Lindelöf space is a Lindelöf set. -/ protected lemma set.is_lindelof [strongly_lindelof_space X] (s : set X) : is_lindelof s := begin intros U hU hsU, @@ -347,16 +380,15 @@ end /-- In a strongly Lindelöf space (e.g., in a space with second countable topology), 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 [strongly_lindelof_space X] - (s : ι → set X) (H : ∀ i, is_open (s i)) : +lemma is_open_Union_countable [strongly_lindelof_space X] (s : ι → set X) (H : ∀ i, is_open (s i)) : ∃ T : set ι, countable T ∧ (⋃ i ∈ T, s i) = ⋃ i, s i := let ⟨T, hTc, hT⟩ := (⋃ i, s i).is_lindelof.countable_open_subcover H subset.rfl in ⟨T, hTc, (Union₂_subset_Union _ _).antisymm hT⟩ /-- In a strongly Lindelöf space (e.g., in a space with second countable topology), an open set, given as a union of open sets, is equal to the union of countably many of those sets. -/ -lemma is_open_sUnion_countable [strongly_lindelof_space X] - (S : set (set X)) (H : ∀ s ∈ S, is_open s) : +lemma is_open_sUnion_countable [strongly_lindelof_space X] (S : set (set X)) + (H : ∀ s ∈ S, is_open s) : ∃ T : set (set X), countable T ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S := let ⟨T, hTS, hTc, hST⟩ := (⋃₀ S).is_lindelof.countable_open_subcover₂ H sUnion_eq_bUnion.subset in ⟨T, hTc, hTS, (sUnion_mono hTS).antisymm (hST.trans sUnion_eq_bUnion.symm.subset)⟩ @@ -365,6 +397,11 @@ lemma countable_cover_nhds_within [strongly_lindelof_space X] {f : X → set X} (hf : ∀ x ∈ s, f x ∈ 𝓝[s] x) : ∃ t ⊆ s, countable t ∧ s ⊆ (⋃ x ∈ t, f x) := s.is_lindelof.countable_cover_nhds_within hf +/-- A countable topological space is a Lindelöf space. -/ +@[priority 100] +instance encodable.strongly_lindelof_space [encodable X] : strongly_lindelof_space X := +⟨λ s hs, (countable_encodable s).is_lindelof⟩ + @[priority 100] instance strongly_lindelof_space.lindelof_space [strongly_lindelof_space X] : lindelof_space X := ⟨set.is_lindelof univ⟩ diff --git a/src/topology/subset_properties.lean b/src/topology/subset_properties.lean index 2e78e7e31a9aa..adee8a87ab7c9 100644 --- a/src/topology/subset_properties.lean +++ b/src/topology/subset_properties.lean @@ -1119,6 +1119,7 @@ end monotone_accumulate h /-- A `σ`-compact topological space is a Lindelöf space. -/ +@[priority 100] -- see Note [lower instance priority] instance sigma_compact_space.lindelof_space [sigma_compact_space α] : lindelof_space α := ⟨Union_compact_covering α ▸ is_lindelof_Union $ λ k, (is_compact_compact_covering α k).is_lindelof⟩ From 6580301925eada9257edab575c59435c481ca87b Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 2 Feb 2022 00:03:59 -0500 Subject: [PATCH 13/15] Fix --- src/topology/subset_properties.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/topology/subset_properties.lean b/src/topology/subset_properties.lean index adee8a87ab7c9..82f3943fc14d9 100644 --- a/src/topology/subset_properties.lean +++ b/src/topology/subset_properties.lean @@ -1120,7 +1120,7 @@ monotone_accumulate h /-- A `σ`-compact topological space is a Lindelöf space. -/ @[priority 100] -- see Note [lower instance priority] -instance sigma_compact_space.lindelof_space [sigma_compact_space α] : lindelof_space α := +instance sigma_compact_space.lindelof_space : lindelof_space α := ⟨Union_compact_covering α ▸ is_lindelof_Union $ λ k, (is_compact_compact_covering α k).is_lindelof⟩ variable {α} From 8a59b507aaa3283d5a0b14f5c05888f78a9d9eba Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 5 Jun 2022 10:53:39 -0400 Subject: [PATCH 14/15] Smaller diff --- src/geometry/manifold/charted_space.lean | 28 ++++++++++++------------ 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/src/geometry/manifold/charted_space.lean b/src/geometry/manifold/charted_space.lean index 1e3adaef15429..dca7d50e3c14b 100644 --- a/src/geometry/manifold/charted_space.lean +++ b/src/geometry/manifold/charted_space.lean @@ -497,20 +497,6 @@ 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 _ _) -open topological_space - -lemma charted_space.second_countable_of_countable_cover [second_countable_topology H] - {s : set M} (hs : (⋃ x (hx : x ∈ s), (chart_at H x).source) = univ) - (hsc : countable s) : - second_countable_topology M := -begin - haveI : ∀ x : M, second_countable_topology (chart_at H x).source := - λ x, (chart_at H x).second_countable_topology_source, - haveI := hsc.to_encodable, - rw bUnion_eq_Union at hs, - exact second_countable_topology_of_countable_cover (λ x : s, (chart_at H (x : M)).open_source) hs -end - variable (M) /-- If a topological space admits an atlas with locally compact charts, then the space itself @@ -529,6 +515,20 @@ begin exact h₂.image_of_continuous_on ((chart_at H x).continuous_on_symm.mono h₃) end +open topological_space + +lemma charted_space.second_countable_of_countable_cover [second_countable_topology H] + {s : set M} (hs : (⋃ x (hx : x ∈ s), (chart_at H x).source) = univ) + (hsc : countable s) : + second_countable_topology M := +begin + haveI : ∀ x : M, second_countable_topology (chart_at H x).source := + λ x, (chart_at H x).second_countable_topology_source, + haveI := hsc.to_encodable, + rw bUnion_eq_Union at hs, + exact second_countable_topology_of_countable_cover (λ x : s, (chart_at H (x : M)).open_source) hs +end + lemma charted_space.second_countable_of_lindelof [second_countable_topology H] [lindelof_space M] : second_countable_topology M := begin From 414c824a27a19c312515656767d6bbdea992bcde Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 5 Jun 2022 21:51:51 -0400 Subject: [PATCH 15/15] Fix --- src/topology/lindelof.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/topology/lindelof.lean b/src/topology/lindelof.lean index a0d02130bd9fe..0ed230d6a6539 100644 --- a/src/topology/lindelof.lean +++ b/src/topology/lindelof.lean @@ -211,7 +211,7 @@ protected lemma set.countable.is_lindelof (hs : countable s) : is_lindelof s := is_lindelof_iff_countable_cover_nhds.mpr $ λ t ht, ⟨s, subset.rfl, hs, λ x hx, mem_Union₂.2 ⟨x, hx, mem_of_mem_nhds (ht x hx)⟩⟩ -protected lemma set.finite.is_lindelof (hs : finite s) : is_lindelof s := +protected lemma set.finite.is_lindelof (hs : s.finite) : is_lindelof s := hs.countable.is_lindelof protected lemma set.subsingleton.is_lindelof (hs : s.subsingleton) : is_lindelof s :=