From 17b2d065eeab325157bf45eb44a1557e965be498 Mon Sep 17 00:00:00 2001 From: PatrickMassot Date: Mon, 13 Apr 2020 08:52:34 +0000 Subject: [PATCH] refactor(order/filter): refactor filters infi and bases (#2384) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR expands what Yury wrote about filter bases, and takes the opportunity to bring long overdue clarification to our treatment of infimums of filters (and also improve documentation and ordering in filter.basic). I'm sorry it mixes reorganization and some new content, but this was hard to avoid (I do keep what motivated all this for a later PR). The fundamental problem is that the infimum construction remained mysterious in filter.basic. All lemmas about it assume a directed family of filters. Yet there are many uses of infimums without this condition, notatably things like `⨅ i, principal (s i)` without condition on the indexed family of sets `s`. Related to this, `filter.generate` stayed mysterious. It was used only as a technical device to lift the complete lattice structure from `set (set a)`. However it has a perfectly valid mathematical existence, as explained by the lemma ```lean lemma sets_iff_generate {s : set (set α)} {f : filter α} : f ≤ filter.generate s ↔ s ⊆ f.sets ``` which justifies the docstring of `generate`: `generate g` is the smallest filter containing the sets `g`. As an example of the mess this created, consider: https://github.com/leanprover-community/mathlib/blob/e758263/src/topology/bases.lean#L25 ```lean def has_countable_basis (f : filter α) : Prop := ∃ s : set (set α), countable s ∧ f = ⨅ t ∈ s, principal t ``` As it stands, this definition is not clearly related to asking for the existence of a countable `s` such that `f = generate s`. Here the main mathematical content this PR adds in this direction: ```lean lemma mem_generate_iff (s : set $ set α) {U : set α} : U ∈ generate s ↔ ∃ t ⊆ s, finite t ∧ ⋂₀ t ⊆ U lemma infi_eq_generate (s : ι → filter α) : infi s = generate (⋃ i, (s i).sets) lemma mem_infi_iff {ι} {s : ι → filter α} {U : set α} : (U ∈ ⨅ i, s i) ↔ ∃ I : set ι, finite I ∧ ∃ V : {i | i ∈ I} → set α, (∀ i, V i ∈ s i) ∧ (⋂ i, V i) ⊆ U ``` All the other changes in filter.basic are either: * moving out stuff that should have been in other files (such as the lemmas that used to be at the very top of this file) * reordering lemmas so that we can have section headers and things are easier to find, * adding to the module docstring. This module docstring contains more mathematical explanation than our usual ones. I feel this is needed because many people think filters are exotic (whereas I'm more and more convinced we should teach filters). The reordering stuff makes it clear we could split this file into a linear chain of files, like we did with topology, but this is open for discussion. Next I added a lot to `filter.bases`. Here the issue is filter bases are used in two different ways. If you already have a filter, but you want to point out it suffices to use certain sets in it. Here you want to use Yury's `has_basis`. Or you can start with a (small) family of sets having nice properties, and build a filter out of it. Currently we don't have this in mathlib, but this is crucial for incoming PRs from the perfectoid project. For instance, in order to define the I-adic topology, you start with powers of I, make a filter and then make a topology. This also reduces the gap with Bourbaki which uses filter bases everywhere. I turned `has_basis` into a single field structure. It makes it very slightly less convenient to prove (you need an extra pair of angle brackets) but much easier to extend when you want to record more properties of the basis, like being countable or decreasing. Also I proved the fundamental property that `f.has_basis p s` implies that `s` (filtered by `p`) actually *is* a filter basis. This is of course easy but crucial to connect with real world maths. At the end of this file, I moved the countable filter basis stuff that is currently in topology.bases (aiming for first countable topologies) except that I used the foundational work on filter.basic to clearly prove all different formulations. In particular: ```lean lemma generate_eq_generate_inter (s : set (set α)) : generate s = generate (sInter '' { t | finite t ∧ t ⊆ s}) ``` clarifies things because the right-hand colleciton is countable if `s` is, and has the nice directedness condition. I also took the opportunity to simplify a proof in topology.sequences, showcasing the power of the newly introduced ```lean lemma has_antimono_basis.tendsto [semilattice_sup ι] [nonempty ι] {l : filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_antimono_basis p s) {φ : ι → α} (h : ∀ i : ι, φ i ∈ s i) : tendsto φ at_top l ``` (I will add more to that sequences file in the next PR). --- docs/theories/topology.md | 2 +- src/data/set/finite.lean | 18 + src/data/set/lattice.lean | 15 + src/measure_theory/bochner_integration.lean | 4 +- src/measure_theory/integration.lean | 2 +- src/measure_theory/set_integral.lean | 4 +- src/order/complete_lattice.lean | 4 + src/order/filter/bases.lean | 505 +++++++++++++++-- src/order/filter/basic.lean | 538 +++++++++++-------- src/order/zorn.lean | 10 + src/topology/bases.lean | 151 +----- src/topology/basic.lean | 2 +- src/topology/continuous_on.lean | 4 +- src/topology/metric_space/basic.lean | 8 +- src/topology/metric_space/emetric_space.lean | 10 +- src/topology/sequences.lean | 52 +- src/topology/uniform_space/cauchy.lean | 6 +- 17 files changed, 886 insertions(+), 449 deletions(-) diff --git a/docs/theories/topology.md b/docs/theories/topology.md index a790b58ad60a7..6ac2bd491dfaa 100644 --- a/docs/theories/topology.md +++ b/docs/theories/topology.md @@ -1,7 +1,7 @@ # Maths in lean : Topological Spaces. The `topological_space` typeclass is defined in mathlib, -in `topology/basic.lean`. There are over 4500 +in `topology/basic.lean`. There are about 18000 lines of code in `topology` at the time of writing, covering the basics of topological spaces, continuous functions, topological groups and rings, and infinite sums. These docs diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean index a560e864fe1ef..71b346e6dedf6 100644 --- a/src/data/set/finite.lean +++ b/src/data/set/finite.lean @@ -368,6 +368,24 @@ begin exact ⟨x, ⟨hx, hf _⟩⟩, end +lemma eq_finite_Union_of_finite_subset_Union {ι} {s : ι → set α} {t : set α} (tfin : finite t) (h : t ⊆ ⋃ i, s i) : + ∃ I : set ι, (finite I) ∧ ∃ σ : {i | i ∈ I} → set α, + (∀ i, finite (σ i)) ∧ (∀ i, σ i ⊆ s i) ∧ t = ⋃ i, σ i := +let ⟨I, Ifin, hI⟩ := finite_subset_Union tfin h in +⟨I, Ifin, λ x, s x ∩ t, + λ i, finite_subset tfin (inter_subset_right _ _), + λ i, inter_subset_left _ _, + begin + ext x, + rw mem_Union, + split, + { intro x_in, + rcases mem_Union.mp (hI x_in) with ⟨i, _, ⟨hi, rfl⟩, H⟩, + use [i, hi, H, x_in] }, + { rintros ⟨i, hi, H⟩, + exact H } + end⟩ + lemma finite_range_ite {p : α → Prop} [decidable_pred p] {f g : α → β} (hf : finite (range f)) (hg : finite (range g)) : finite (range (λ x, if p x then f x else g x)) := finite_subset (finite_union hf hg) range_ite_subset diff --git a/src/data/set/lattice.lean b/src/data/set/lattice.lean index af5e13b4a3bca..a2bf918c2c432 100644 --- a/src/data/set/lattice.lean +++ b/src/data/set/lattice.lean @@ -197,6 +197,14 @@ theorem diff_Inter (s : set β) (t : ι → set β) : s \ (⋂ i, t i) = ⋃ i, s \ t i := by rw [diff_eq, compl_Inter, inter_Union]; refl +lemma directed_on_Union {r} {ι : Sort v} {f : ι → set α} (hd : directed (⊆) f) + (h : ∀x, directed_on r (f x)) : directed_on r (⋃x, f x) := +by simp only [directed_on, exists_prop, mem_Union, exists_imp_distrib]; exact +assume a₁ b₁ fb₁ a₂ b₂ fb₂, +let ⟨z, zb₁, zb₂⟩ := hd b₁ b₂, + ⟨x, xf, xa₁, xa₂⟩ := h z a₁ (zb₁ fb₁) a₂ (zb₂ fb₂) in +⟨x, ⟨z, xf⟩, xa₁, xa₂⟩ + /- bounded unions and intersections -/ theorem mem_bUnion_iff {s : set α} {t : α → set β} {y : β} : @@ -385,6 +393,13 @@ 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 @[simp] theorem sInter_insert (s : set α) (T : set (set α)) : ⋂₀ (insert s T) = s ∩ ⋂₀ T := Inf_insert diff --git a/src/measure_theory/bochner_integration.lean b/src/measure_theory/bochner_integration.lean index 29cfdb7d7987e..ba96c9bcc3993 100644 --- a/src/measure_theory/bochner_integration.lean +++ b/src/measure_theory/bochner_integration.lean @@ -1026,7 +1026,7 @@ variables [normed_group β] [second_countable_topology β] [normed_space ℝ β] [measurable_space β] [borel_space β] [normed_group γ] [second_countable_topology γ] [normed_space ℝ γ] [complete_space γ] [measurable_space γ] [borel_space γ] - + /-- The Bochner integral -/ def integral (f : α → β) : β := if hf : measurable f ∧ integrable f @@ -1151,7 +1151,7 @@ end /-- Lebesgue dominated convergence theorem for filters with a countable basis -/ lemma tendsto_integral_filter_of_dominated_convergence {ι} {l : filter ι} {F : ι → α → β} {f : α → β} (bound : α → ℝ) - (hl_cb : l.has_countable_basis) + (hl_cb : l.is_countably_generated) (hF_meas : ∀ᶠ n in l, measurable (F n)) (f_measurable : measurable f) (h_bound : ∀ᶠ n in l, ∀ₘ a, ∥F n a∥ ≤ bound a) diff --git a/src/measure_theory/integration.lean b/src/measure_theory/integration.lean index bf26a73a00be0..537ed59ed1e17 100644 --- a/src/measure_theory/integration.lean +++ b/src/measure_theory/integration.lean @@ -1177,7 +1177,7 @@ end /-- Dominated convergence theorem for filters with a countable basis -/ lemma tendsto_lintegral_filter_of_dominated_convergence {ι} {l : filter ι} {F : ι → α → ennreal} {f : α → ennreal} (bound : α → ennreal) - (hl_cb : l.has_countable_basis) + (hl_cb : l.is_countably_generated) (hF_meas : ∀ᶠ n in l, measurable (F n)) (h_bound : ∀ᶠ n in l, ∀ₘ a, F n a ≤ bound a) (h_fin : lintegral bound < ⊤) diff --git a/src/measure_theory/set_integral.lean b/src/measure_theory/set_integral.lean index ceba7c4f974e6..dc105caec272b 100644 --- a/src/measure_theory/set_integral.lean +++ b/src/measure_theory/set_integral.lean @@ -306,7 +306,7 @@ begin end -- TODO : prove this for an encodable type --- by proving an encodable version of `filter.has_countable_basis_at_top_finset_nat` +-- by proving an encodable version of `filter.is_countably_generated_at_top_finset_nat ` lemma integral_on_Union (s : ℕ → set α) (f : α → β) (hm : ∀i, is_measurable (s i)) (hd : ∀ i j, i ≠ j → s i ∩ s j = ∅) (hfm : measurable_on (Union s) f) (hfi : integrable_on (Union s) f) : (∫ a in (Union s), f a) = ∑i, ∫ a in s i, f a := @@ -322,7 +322,7 @@ begin rw this, refine tendsto_integral_filter_of_dominated_convergence _ _ _ _ _ _ _, { exact indicator (Union s) (λ a, ∥f a∥) }, - { exact has_countable_basis_at_top_finset_nat }, + { exact is_countably_generated_at_top_finset_nat }, { refine univ_mem_sets' (λ n, _), simp only [mem_set_of_eq], refine hfm.subset (is_measurable.Union (λ i, is_measurable.Union_Prop (λh, hm _))) diff --git a/src/order/complete_lattice.lean b/src/order/complete_lattice.lean index 8c85d842295db..6546636c8a69d 100644 --- a/src/order/complete_lattice.lean +++ b/src/order/complete_lattice.lean @@ -667,6 +667,10 @@ lemma infi_subtype' {p : ι → Prop} {f : ∀ i, p i → α} : (⨅ i (h : p i), f i h) = (⨅ x : subtype p, f x.val x.property) := (@infi_subtype _ _ _ p (λ x, f x.val x.property)).symm +lemma infi_subtype'' {ι} (s : set ι) (f : ι → α) : +(⨅ i : s, f i) = ⨅ (t : ι) (H : t ∈ s), f t := +infi_subtype + theorem supr_subtype {p : ι → Prop} {f : subtype p → α} : (⨆ x, f x) = (⨆ i (h:p i), f ⟨i, h⟩) := le_antisymm (supr_le $ assume ⟨i, h⟩, le_supr_of_le i $ le_supr (λh:p i, f ⟨i, h⟩) _) diff --git a/src/order/filter/bases.lean b/src/order/filter/bases.lean index f950acea0e7f4..c2ffc57291c90 100644 --- a/src/order/filter/bases.lean +++ b/src/order/filter/bases.lean @@ -1,15 +1,34 @@ /- Copyright (c) 2020 Yury Kudryashov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Yury Kudryashov +Author: Yury Kudryashov, Johannes Hölzl, Mario Carneiro, Patrick Massot -/ -import order.filter.basic +import order.filter.basic data.set.countable /-! # Filter bases -In this file we define `filter.has_basis l p s`, where `l` is a filter on `α`, `p` is a predicate -on some index set `ι`, and `s : ι → set α`. +A filter basis `B : filter_basis α` on a type `α` is a nonempty collection of sets of `α` +such that the intersection of two elements of this collection contains some element of +the collection. Compared to filters, filter bases do not require that any set containing +an element of `B` belongs to `B`. +A filter basis `B` can be used to construct `B.filter : filter α` such that a set belongs +to `B.filter` if and only if it contains an element of `B`. + +Given an indexing type `ι`, a predicate `p : ι → Prop`, and a map `s : ι → set α`, +the proposition `h : filter.is_basis p s` makes sure the range of `s` bounded by `p` +(ie. `s '' set_of p`) defines a filter basis `h.filter_basis`. + +If one already has a filter `l` on `α`, `filter.has_basis l p s` (where `p : ι → Prop` +and `s : ι → set α` as above) means that a set belongs to `l` if and +only if it contains some `s i` with `p i`. It implies `h : filter.is_basis p s`, and +`l = h.filter_basis.filter`. The point of this definition is that checking statements +involving elements of `l` often reduces to checking them on the basis elements. + +This file also introduces more restricted classes of bases, involving monotonicity or +countability. In particular, for `l : filter α`, `l.is_countably_generated` means +there is a countable set of sets which generates `s`. This is reformulated in term of bases, +and consequences are derived. ## Main statements @@ -23,6 +42,10 @@ on some index set `ι`, and `s : ι → set α`. of bases. * `has_basis.tendsto_right_iff`, `has_basis.tendsto_left_iff`, `has_basis.tendsto_iff` : restate `tendsto f l l'` in terms of bases. +* `is_countably_generated_iff_exists_antimono_basis` : proves a filter is + countably generated if and only if it admis a basis parametrized by a + decreasing sequence of sets indexed by `ℕ`. +* `tendsto_iff_seq_tendsto ` : an abstract version of "sequentially continuous implies continuous". ## Implementation notes @@ -40,57 +63,204 @@ machinery, e.g., `simp only [exists_prop, true_and]` or `simp only [forall_const with the case `p = λ _, true`. -/ -namespace filter +open set filter + variables {α : Type*} {β : Type*} {γ : Type*} {ι : Type*} {ι' : Type*} -open set +/-- A filter basis `B` on a type `α` is a nonempty collection of sets of `α` +such that the intersection of two elements of this collection contains some element +of the collection. -/ +structure filter_basis (α : Type*) := +(sets : set (set α)) +(nonempty : sets.nonempty) +(inter_sets {x y} : x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y) + +/-- If `B` is a filter basis on `α`, and `U` a subset of `α` then we can write `U ∈ B` as on paper. -/ +@[reducible] +instance {α : Type*}: has_mem (set α) (filter_basis α) := ⟨λ U B, U ∈ B.sets⟩ + +-- For illustration purposes, the filter basis defining (at_top : filter ℕ) +instance : inhabited (filter_basis ℕ) := +⟨{ sets := range Ici, + nonempty := ⟨Ici 0, mem_range_self 0⟩, + inter_sets := begin + rintros _ _ ⟨n, rfl⟩ ⟨m, rfl⟩, + refine ⟨Ici (max n m), mem_range_self _, _⟩, + rintros p p_in, + split ; rw mem_Ici at *, + exact le_of_max_le_left p_in, + exact le_of_max_le_right p_in, + end }⟩ + +/-- `is_basis p s` means the image of `s` bounded by `p` is a filter basis. -/ +protected structure filter.is_basis (p : ι → Prop) (s : ι → set α) : Prop := +(nonempty : ∃ i, p i) +(inter : ∀ {i j}, p i → p j → ∃ k, p k ∧ s k ⊆ s i ∩ s j) + +namespace filter +namespace is_basis + +/-- Constructs a filter basis from an indexed family of sets satisfying `is_basis`. -/ +protected def filter_basis {p : ι → Prop} {s : ι → set α} (h : is_basis p s) : filter_basis α := +{ sets := s '' set_of p, + nonempty := let ⟨i, hi⟩ := h.nonempty in ⟨s i, mem_image_of_mem s hi⟩, + inter_sets := by { rintros _ _ ⟨i, hi, rfl⟩ ⟨j, hj, rfl⟩, + rcases h.inter hi hj with ⟨k, hk, hk'⟩, + exact ⟨_, mem_image_of_mem s hk, hk'⟩ } } + +variables {p : ι → Prop} {s : ι → set α} (h : is_basis p s) + +lemma mem_filter_basis_iff {U : set α} : U ∈ h.filter_basis ↔ ∃ i, p i ∧ s i = U := +iff.rfl +end is_basis +end filter + +namespace filter_basis + +/-- The filter associated to a filter basis. -/ +protected def filter (B : filter_basis α) : filter α := +{ sets := {s | ∃ t ∈ B, t ⊆ s}, + univ_sets := let ⟨s, s_in⟩ := B.nonempty in ⟨s, s_in, s.subset_univ⟩, + sets_of_superset := λ x y ⟨s, s_in, h⟩ hxy, ⟨s, s_in, set.subset.trans h hxy⟩, + inter_sets := λ x y ⟨s, s_in, hs⟩ ⟨t, t_in, ht⟩, + let ⟨u, u_in, u_sub⟩ := B.inter_sets s_in t_in in + ⟨u, u_in, set.subset.trans u_sub $ set.inter_subset_inter hs ht⟩ } + +lemma mem_filter_iff (B : filter_basis α) {U : set α} : U ∈ B.filter ↔ ∃ s ∈ B, s ⊆ U := +iff.rfl + +lemma mem_filter_of_mem (B : filter_basis α) {U : set α} : U ∈ B → U ∈ B.filter:= +λ U_in, ⟨U, U_in, subset.refl _⟩ + +lemma eq_infi_principal (B : filter_basis α) : B.filter = ⨅ s : B.sets, principal s := +begin + ext U, + rw [mem_filter_iff, mem_infi], + { simp }, + { rintros ⟨U, U_in⟩ ⟨V, V_in⟩, + rcases B.inter_sets U_in V_in with ⟨W, W_in, W_sub⟩, + use [W, W_in], + finish }, + cases B.nonempty with U U_in, + exact ⟨⟨U, U_in⟩⟩, +end + +protected lemma generate (B : filter_basis α) : generate B.sets = B.filter := +begin + apply le_antisymm, + { intros U U_in, + rcases B.mem_filter_iff.mp U_in with ⟨V, V_in, h⟩, + exact generate_sets.superset (generate_sets.basic V_in) h }, + { rw sets_iff_generate, + apply mem_filter_of_mem } +end +end filter_basis + +namespace filter +namespace is_basis +variables {p : ι → Prop} {s : ι → set α} + +/-- Constructs a filter from an indexed family of sets satisfying `is_basis`. -/ +protected def filter (h : is_basis p s) : filter α := h.filter_basis.filter + +protected lemma mem_filter_iff (h : is_basis p s) {U : set α} : + U ∈ h.filter ↔ ∃ i, p i ∧ s i ⊆ U := +begin + erw [h.filter_basis.mem_filter_iff], + simp only [mem_filter_basis_iff h, exists_prop], + split, + { rintros ⟨_, ⟨i, pi, rfl⟩, h⟩, + tauto }, + { tauto } +end + +lemma filter_eq_generate (h : is_basis p s) : h.filter = generate {U | ∃ i, p i ∧ s i = U} := +by erw h.filter_basis.generate ; refl +end is_basis /-- We say that a filter `l` has a basis `s : ι → set α` bounded by `p : ι → Prop`, if `t ∈ l` if and only if `t` includes `s i` for some `i` such that `p i`. -/ -protected def has_basis (l : filter α) (p : ι → Prop) (s : ι → set α) : Prop := -∀ t : set α, t ∈ l ↔ ∃ i (hi : p i), s i ⊆ t +protected structure has_basis (l : filter α) (p : ι → Prop) (s : ι → set α) : Prop := +(mem_iff' : ∀ (t : set α), t ∈ l ↔ ∃ i (hi : p i), s i ⊆ t) section same_type variables {l l' : filter α} {p : ι → Prop} {s : ι → set α} {t : set α} {i : ι} {p' : ι' → Prop} {s' : ι' → set α} {i' : ι'} -/-- Definition of `has_basis` unfolded to make it useful for `rw` and `simp`. -/ +lemma has_basis_generate (s : set (set α)) : (generate s).has_basis (λ t, finite t ∧ t ⊆ s) (λ t, ⋂₀ t) := +⟨begin + intro U, + rw mem_generate_iff, + apply exists_congr, + tauto +end⟩ + +/-- The smallest filter basis containing a given collection of sets. -/ +def filter_basis.of_sets (s : set (set α)) : filter_basis α := +{ sets := sInter '' { t | finite t ∧ t ⊆ s}, + nonempty := ⟨univ, ∅, ⟨⟨finite_empty, empty_subset s⟩, sInter_empty⟩⟩, + inter_sets := begin + rintros _ _ ⟨a, ⟨fina, suba⟩, rfl⟩ ⟨b, ⟨finb, subb⟩, rfl⟩, + exact ⟨⋂₀ (a ∪ b), mem_image_of_mem _ ⟨finite_union fina finb, union_subset suba subb⟩, + by rw sInter_union⟩, + end } + +/-- Definition of `has_basis` unfolded with implicit set argument. -/ lemma has_basis.mem_iff (hl : l.has_basis p s) : t ∈ l ↔ ∃ i (hi : p i), s i ⊆ t := -hl t +hl.mem_iff' t -lemma has_basis.eventually_iff (hl : l.has_basis p s) {q : α → Prop} : - (∀ᶠ x in l, q x) ↔ ∃ i (hi : p i), ∀ ⦃x⦄, x ∈ s i → q x := -hl _ +protected lemma is_basis.has_basis (h : is_basis p s) : has_basis h.filter p s := +⟨λ t, by simp only [h.mem_filter_iff, exists_prop]⟩ lemma has_basis.mem_of_superset (hl : l.has_basis p s) (hi : p i) (ht : s i ⊆ t) : t ∈ l := -(hl t).2 ⟨i, hi, ht⟩ +(hl.mem_iff).2 ⟨i, hi, ht⟩ lemma has_basis.mem_of_mem (hl : l.has_basis p s) (hi : p i) : s i ∈ l := hl.mem_of_superset hi $ subset.refl _ +lemma has_basis.is_basis (h : l.has_basis p s) : is_basis p s := +{ nonempty := let ⟨i, hi, H⟩ := h.mem_iff.mp univ_mem_sets in ⟨i, hi⟩, + inter := λ i j hi hj, by simpa [h.mem_iff] using l.inter_sets (h.mem_of_mem hi) (h.mem_of_mem hj) } + +lemma has_basis.filter_eq (h : l.has_basis p s) : h.is_basis.filter = l := +by { ext U, simp [h.mem_iff, is_basis.mem_filter_iff] } + +lemma has_basis.eq_generate (h : l.has_basis p s) : l = generate { U | ∃ i, p i ∧ s i = U } := +by rw [← h.is_basis.filter_eq_generate, h.filter_eq] + +lemma generate_eq_generate_inter (s : set (set α)) : generate s = generate (sInter '' { t | finite t ∧ t ⊆ s}) := +by erw [(filter_basis.of_sets s).generate, ← (has_basis_generate s).filter_eq] ; refl + +lemma of_sets_filter_eq_generate (s : set (set α)) : (filter_basis.of_sets s).filter = generate s := +by rw [← (filter_basis.of_sets s).generate, generate_eq_generate_inter s] ; refl + +lemma has_basis.eventually_iff (hl : l.has_basis p s) {q : α → Prop} : + (∀ᶠ x in l, q x) ↔ ∃ i, p i ∧ ∀ ⦃x⦄, x ∈ s i → q x := +by simpa using hl.mem_iff + lemma has_basis.forall_nonempty_iff_ne_bot (hl : l.has_basis p s) : (∀ {i}, p i → (s i).nonempty) ↔ l ≠ ⊥ := ⟨λ H, forall_sets_nonempty_iff_ne_bot.1 $ - λ s hs, let ⟨i, hi, his⟩ := (hl s).1 hs in (H hi).mono his, + λ s hs, let ⟨i, hi, his⟩ := hl.mem_iff.1 hs in (H hi).mono his, λ H i hi, nonempty_of_mem_sets H (hl.mem_of_mem hi)⟩ lemma basis_sets (l : filter α) : l.has_basis (λ s : set α, s ∈ l) id := -λ t, exists_sets_subset_iff.symm +⟨λ t, exists_sets_subset_iff.symm⟩ lemma at_top_basis [nonempty α] [semilattice_sup α] : (@at_top α _).has_basis (λ _, true) Ici := -λ t, by simpa only [exists_prop, true_and] using @mem_at_top_sets α _ _ t +⟨λ t, by simpa only [exists_prop, true_and] using @mem_at_top_sets α _ _ t⟩ lemma at_top_basis' [semilattice_sup α] (a : α) : (@at_top α _).has_basis (λ x, a ≤ x) Ici := -λ t, (@at_top_basis α ⟨a⟩ _ t).trans +⟨λ t, (@at_top_basis α ⟨a⟩ _).mem_iff.trans ⟨λ ⟨x, _, hx⟩, ⟨x ⊔ a, le_sup_right, λ y hy, hx (le_trans le_sup_left hy)⟩, - λ ⟨x, _, hx⟩, ⟨x, trivial, hx⟩⟩ + λ ⟨x, _, hx⟩, ⟨x, trivial, hx⟩⟩⟩ theorem has_basis.ge_iff (hl' : l'.has_basis p' s') : l ≤ l' ↔ ∀ i', p' i' → s' i' ∈ l := ⟨λ h i' hi', h $ hl'.mem_of_mem hi', - λ h s hs, let ⟨i', hi', hs⟩ := (hl' s).1 hs in mem_sets_of_superset (h _ hi') hs⟩ + λ h s hs, let ⟨i', hi', hs⟩ := hl'.mem_iff.1 hs in mem_sets_of_superset (h _ hi') hs⟩ theorem has_basis.le_iff (hl : l.has_basis p s) : l ≤ l' ↔ ∀ t ∈ l', ∃ i (hi : p i), s i ⊆ t := by simp only [le_def, hl.mem_iff] @@ -101,7 +271,7 @@ by simp only [hl'.ge_iff, hl.mem_iff] lemma has_basis.inf (hl : l.has_basis p s) (hl' : l'.has_basis p' s') : (l ⊓ l').has_basis (λ i : ι × ι', p i.1 ∧ p' i.2) (λ i, s i.1 ∩ s' i.2) := -begin +⟨begin intro t, simp only [mem_inf_sets, exists_prop, hl.mem_iff, hl'.mem_iff], split, @@ -109,12 +279,12 @@ begin use [(i, i'), ⟨hi, hi'⟩, subset.trans (inter_subset_inter ht ht') H] }, { rintros ⟨⟨i, i'⟩, ⟨hi, hi'⟩, H⟩, use [s i, i, hi, subset.refl _, s' i', i', hi', subset.refl _, H] } -end +end⟩ lemma has_basis.inf_principal (hl : l.has_basis p s) (s' : set α) : (l ⊓ principal s').has_basis p (λ i, s i ∩ s') := -λ t, by simp only [mem_inf_principal, hl.mem_iff, subset_def, mem_set_of_eq, - mem_inter_iff, and_imp] +⟨λ t, by simp only [mem_inf_principal, hl.mem_iff, subset_def, mem_set_of_eq, + mem_inter_iff, and_imp]⟩ lemma has_basis.eq_binfi (h : l.has_basis p s) : l = ⨅ i (_ : p i), principal (s i) := @@ -127,30 +297,30 @@ by simpa only [infi_true] using h.eq_binfi @[nolint ge_or_gt] -- see Note [nolint_ge] lemma has_basis_infi_principal {s : ι → set α} (h : directed (≥) s) (ne : nonempty ι) : (⨅ i, principal (s i)).has_basis (λ _, true) s := -begin +⟨begin refine λ t, (mem_infi (h.mono_comp _ _) ne t).trans $ by simp only [exists_prop, true_and, mem_principal_sets], exact λ _ _, principal_mono.2 -end +end⟩ @[nolint ge_or_gt] -- see Note [nolint_ge] lemma has_basis_binfi_principal {s : β → set α} {S : set β} (h : directed_on (s ⁻¹'o (≥)) S) (ne : S.nonempty) : (⨅ i ∈ S, principal (s i)).has_basis (λ i, i ∈ S) s := -begin +⟨begin refine λ t, (mem_binfi _ ne).trans $ by simp only [mem_principal_sets], rw [directed_on_iff_directed, ← directed_comp, (∘)] at h ⊢, apply h.mono_comp _ _, exact λ _ _, principal_mono.2 -end +end⟩ lemma has_basis.map (f : α → β) (hl : l.has_basis p s) : (l.map f).has_basis p (λ i, f '' (s i)) := -λ t, by simp only [mem_map, image_subset_iff, hl.mem_iff, preimage] +⟨λ t, by simp only [mem_map, image_subset_iff, hl.mem_iff, preimage]⟩ lemma has_basis.comap (f : β → α) (hl : l.has_basis p s) : (l.comap f).has_basis p (λ i, f ⁻¹' (s i)) := -begin +⟨begin intro t, simp only [mem_comap_sets, exists_prop, hl.mem_iff], split, @@ -158,11 +328,11 @@ begin exact ⟨i, hi, subset.trans (preimage_mono ht') H⟩ }, { rintros ⟨i, hi, H⟩, exact ⟨s i, ⟨i, hi, subset.refl _⟩, H⟩ } -end +end⟩ lemma has_basis.prod_self (hl : l.has_basis p s) : (l.prod l).has_basis p (λ i, (s i).prod (s i)) := -begin +⟨begin intro t, apply mem_prod_iff.trans, split, @@ -171,8 +341,22 @@ begin exact ⟨i, hi, λ p ⟨hp₁, hp₂⟩, H ⟨(ht hp₁).1, (ht hp₂).2⟩⟩ }, { rintros ⟨i, hi, H⟩, exact ⟨s i, hl.mem_of_mem hi, s i, hl.mem_of_mem hi, H⟩ } -end - +end⟩ +variables [preorder ι] (l p s) + +/-- `is_antimono_basis p s` means the image of `s` bounded by `p` is a filter basis +such that `s` is decreasing and `p` is increasing, ie `i ≤ j → p i → p j`. -/ +structure is_antimono_basis extends is_basis p s : Prop := +(decreasing : ∀ {i j}, p i → p j → i ≤ j → s j ⊆ s i) +(mono : monotone p) + +/-- We say that a filter `l` has a antimono basis `s : ι → set α` bounded by `p : ι → Prop`, +if `t ∈ l` if and only if `t` includes `s i` for some `i` such that `p i`, +and `s` is decreasing and `p` is increasing, ie `i ≤ j → p i → p j`. -/ +structure has_antimono_basis [preorder ι] (l : filter α) (p : ι → Prop) (s : ι → set α) + extends has_basis l p s : Prop := +(decreasing : ∀ {i j}, p i → p j → i ≤ j → s j ⊆ s i) +(mono : monotone p) end same_type section two_types @@ -190,7 +374,7 @@ by simp only [tendsto, hlb.ge_iff, mem_map, filter.eventually] lemma has_basis.tendsto_iff (hla : la.has_basis pa sa) (hlb : lb.has_basis pb sb) : tendsto f la lb ↔ ∀ ib (hib : pb ib), ∃ ia (hia : pa ia), ∀ x ∈ sa ia, f x ∈ sb ib := -by simp only [hlb.tendsto_right_iff, hla.eventually_iff, subset_def, mem_set_of_eq] +by simp [hlb.tendsto_right_iff, hla.eventually_iff] lemma tendsto.basis_left (H : tendsto f la lb) (hla : la.has_basis pa sa) : ∀ t ∈ lb, ∃ i (hi : pa i), ∀ x ∈ sa i, f x ∈ t := @@ -209,6 +393,257 @@ lemma has_basis.prod (hla : la.has_basis pa sa) (hlb : lb.has_basis pb sb) : (la.prod lb).has_basis (λ i : ι × ι', pa i.1 ∧ pb i.2) (λ i, (sa i.1).prod (sb i.2)) := (hla.comap prod.fst).inf (hlb.comap prod.snd) +lemma has_antimono_basis.tendsto [semilattice_sup ι] [nonempty ι] {l : filter α} + {p : ι → Prop} {s : ι → set α} (hl : l.has_antimono_basis p s) {φ : ι → α} + (h : ∀ i : ι, φ i ∈ s i) : tendsto φ at_top l := +begin + rw hl.to_has_basis.tendsto_right_iff, + intros i hi, + rw eventually_at_top, + exact ⟨i, λ j hij, hl.decreasing hi (hl.mono hij hi) hij (h j)⟩, +end + end two_types +/-- `is_countably_generated f` means `f = generate s` for some countable `s`. -/ +def is_countably_generated (f : filter α) : Prop := +∃ s : set (set α), countable s ∧ f = generate s + +/-- `is_countable_basis p s` means the image of `s` bounded by `p` is a countable filter basis. -/ +structure is_countable_basis (p : ι → Prop) (s : ι → set α) extends is_basis p s : Prop := +(countable : countable $ set_of p) + +/-- We say that a filter `l` has a countable basis `s : ι → set α` bounded by `p : ι → Prop`, +if `t ∈ l` if and only if `t` includes `s i` for some `i` such that `p i`, and the set +defined by `p` is countable. -/ +structure has_countable_basis (l : filter α) (p : ι → Prop) (s : ι → set α) extends has_basis l p s : Prop := +(countable : countable $ set_of p) + +/-- A countable filter basis `B` on a type `α` is a nonempty countable collection of sets of `α` +such that the intersection of two elements of this collection contains some element +of the collection. -/ +structure countable_filter_basis (α : Type*) extends filter_basis α := +(countable : countable sets) + +-- For illustration purposes, the countable filter basis defining (at_top : filter ℕ) +instance nat.inhabited_countable_filter_basis : inhabited (countable_filter_basis ℕ) := +⟨{ countable := countable_range (λ n, Ici n), + ..(default $ filter_basis ℕ),}⟩ + +lemma antimono_seq_of_seq (s : ℕ → set α) : + ∃ t : ℕ → set α, (∀ i j, i ≤ j → t j ⊆ t i) ∧ (⨅ i, principal $ s i) = ⨅ i, principal (t i) := +begin + use λ n, ⋂ m ≤ n, s m, split, + { intros i j hij a, simp, intros h i' hi'i, apply h, transitivity; assumption }, + apply le_antisymm; rw le_infi_iff; intro i, + { rw le_principal_iff, apply Inter_mem_sets (finite_le_nat _), + intros j hji, rw ← le_principal_iff, apply infi_le_of_le j _, apply le_refl _ }, + { apply infi_le_of_le i _, rw principal_mono, intro a, simp, intro h, apply h, refl }, +end + +lemma countable_binfi_eq_infi_seq [complete_lattice α] {B : set ι} (Bcbl : countable B) (Bne : B.nonempty) (f : ι → α) + : ∃ (x : ℕ → ι), (⨅ t ∈ B, f t) = ⨅ i, f (x i) := +begin + rw countable_iff_exists_surjective_to_subtype Bne at Bcbl, + rcases Bcbl with ⟨g, gsurj⟩, + rw infi_subtype', + use (λ n, g n), apply le_antisymm; rw le_infi_iff, + { intro i, apply infi_le_of_le (g i) _, apply le_refl _ }, + { intros a, rcases gsurj a with i, apply infi_le_of_le i _, subst h, apply le_refl _ } +end + +lemma countable_binfi_eq_infi_seq' [complete_lattice α] {B : set ι} (Bcbl : countable B) (f : ι → α) +{i₀ : ι} (h : f i₀ = ⊤) : + ∃ (x : ℕ → ι), (⨅ t ∈ B, f t) = ⨅ i, f (x i) := +begin + cases B.eq_empty_or_nonempty with hB Bnonempty, + { rw [hB, infi_emptyset], + use λ n, i₀, + simp [h] }, + { exact countable_binfi_eq_infi_seq Bcbl Bnonempty f } +end + +lemma countable_binfi_principal_eq_seq_infi {B : set (set α)} (Bcbl : countable B) : + ∃ (x : ℕ → set α), (⨅ t ∈ B, principal t) = ⨅ i, principal (x i) := +countable_binfi_eq_infi_seq' Bcbl principal principal_univ + +namespace is_countably_generated + +/-- A set generating a countably generated filter. -/ +def generating_set {f : filter α} (h : is_countably_generated f) := +classical.some h + +lemma countable_generating_set {f : filter α} (h : is_countably_generated f) : + countable h.generating_set := +(classical.some_spec h).1 + +lemma eq_generate {f : filter α} (h : is_countably_generated f) : + f = generate h.generating_set := +(classical.some_spec h).2 + +/-- A countable filter basis for a countably generated filter. -/ +def countable_filter_basis {l : filter α} (h : is_countably_generated l) : countable_filter_basis α := +{ countable := countable_image _ (countable_set_of_finite_subset h.countable_generating_set), + ..filter_basis.of_sets (h.generating_set) } + +lemma filter_basis_filter {l : filter α} (h : is_countably_generated l) : +h.countable_filter_basis.to_filter_basis.filter = l := +begin + conv_rhs { rw h.eq_generate }, + apply of_sets_filter_eq_generate, +end + +lemma has_countable_basis {l : filter α} (h : is_countably_generated l) : + l.has_countable_basis (λ t, finite t ∧ t ⊆ h.generating_set) (λ t, ⋂₀ t) := +⟨by convert has_basis_generate _ ; exact h.eq_generate, + countable_set_of_finite_subset h.countable_generating_set⟩ + +lemma exists_countable_infi_principal {f : filter α} (h : f.is_countably_generated) : +∃ s : set (set α), countable s ∧ f = ⨅ t ∈ s, principal t := +begin + let B := h.countable_filter_basis, + use [B.sets, B.countable], + rw ← h.filter_basis_filter, + rw B.to_filter_basis.eq_infi_principal, + rw infi_subtype'' +end + +lemma exists_seq {f : filter α} (cblb : f.is_countably_generated) : + ∃ x : ℕ → set α, f = ⨅ i, principal (x i) := +begin + rcases cblb.exists_countable_infi_principal with ⟨B, Bcbl, rfl⟩, + exact countable_binfi_principal_eq_seq_infi Bcbl, +end + +lemma exists_antimono_seq {f : filter α} (cblb : f.is_countably_generated) : + ∃ x : ℕ → set α, (∀ i j, i ≤ j → x j ⊆ x i) ∧ f = ⨅ i, principal (x i) := +begin + rcases cblb.exists_seq with ⟨x', hx'⟩, + let x := λ n, ⋂ m ≤ n, x' m, + use x, split, + { intros i j hij a, simp [x], intros h i' hi'i, apply h, transitivity; assumption }, + subst hx', apply le_antisymm; rw le_infi_iff; intro i, + { rw le_principal_iff, apply Inter_mem_sets (finite_le_nat _), + intros j hji, rw ← le_principal_iff, apply infi_le_of_le j _, apply le_refl _ }, + { apply infi_le_of_le i _, rw principal_mono, intro a, simp [x], intro h, apply h, refl }, +end + +lemma has_antimono_basis {f : filter α} (h : f.is_countably_generated) : + ∃ x : ℕ → set α, f.has_antimono_basis (λ _, true) x := +begin + rcases h.exists_antimono_seq with ⟨x, x_dec, rfl⟩, + use x, + constructor, + apply has_basis_infi_principal, + apply directed_of_mono, apply x_dec, + use 0, + simpa using x_dec, + exact monotone_const +end + +end is_countably_generated + +lemma is_countably_generated_seq (x : ℕ → set α) : is_countably_generated (⨅ i, principal $ x i) := +begin + rcases antimono_seq_of_seq x with ⟨y, am, h⟩, + rw h, + use [range y, countable_range _], + rw (has_basis_infi_principal _ _).eq_generate, + { simp [range] }, + { apply directed_of_mono, apply am }, + { use 0 }, +end + +lemma is_countably_generated_of_seq {f : filter α} (h : ∃ x : ℕ → set α, f = ⨅ i, principal $ x i) : + f.is_countably_generated := +let ⟨x, h⟩ := h in by rw h ; apply is_countably_generated_seq + +lemma is_countably_generated_binfi_principal {B : set $ set α} (h : countable B) : + is_countably_generated (⨅ (s ∈ B), principal s) := +is_countably_generated_of_seq (countable_binfi_principal_eq_seq_infi h) + +lemma is_countably_generated_iff_exists_antimono_basis {f : filter α} : is_countably_generated f ↔ + ∃ x : ℕ → set α, f.has_antimono_basis (λ _, true) x := +begin + split, + { intro h, + exact h.has_antimono_basis }, + { rintros ⟨x, h⟩, + rw h.to_has_basis.eq_infi, + exact is_countably_generated_seq x }, +end + +namespace is_countably_generated + +lemma exists_antimono_seq' {f : filter α} (cblb : f.is_countably_generated) : + ∃ x : ℕ → set α, (∀ i j, i ≤ j → x j ⊆ x i) ∧ ∀ {s}, (s ∈ f ↔ ∃ i, x i ⊆ s) := +let ⟨x, hx⟩ := is_countably_generated_iff_exists_antimono_basis.mp cblb in +⟨x, λ i j, hx.decreasing trivial trivial, λ s, by simp [hx.to_has_basis.mem_iff]⟩ + +protected lemma comap {l : filter β} (h : l.is_countably_generated) (f : α → β) : + (comap f l).is_countably_generated := +begin + rcases h.exists_seq with ⟨x, hx⟩, + apply is_countably_generated_of_seq, + use λ i, f ⁻¹' x i, + calc + comap f l = comap f (⨅ i, principal (x i)) : by rw hx + ... = (⨅ i, comap f $ principal $ x i) : comap_infi + ... = (⨅ i, principal $ f ⁻¹' x i) : by simp_rw comap_principal, +end + +/-- An abstract version of continuity of sequentially continuous functions on metric spaces: +if a filter `k` is countably generated then `tendsto f k l` iff for every sequence `u` +converging to `k`, `f ∘ u` tends to `l`. -/ +lemma tendsto_iff_seq_tendsto {f : α → β} {k : filter α} {l : filter β} + (hcb : k.is_countably_generated) : + tendsto f k l ↔ (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) := +suffices (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) → tendsto f k l, + from ⟨by intros; apply tendsto.comp; assumption, by assumption⟩, +begin + rcases hcb.exists_antimono_seq with ⟨g, gmon, gbasis⟩, + have gbasis : ∀ A, A ∈ k ↔ ∃ i, g i ⊆ A, + { intro A, + subst gbasis, + rw mem_infi, + { simp only [set.mem_Union, iff_self, filter.mem_principal_sets] }, + { exact directed_of_mono _ (λ i j h, principal_mono.mpr $ gmon _ _ h) }, + { apply_instance } }, + classical, contrapose, + simp only [not_forall, not_imp, not_exists, subset_def, @tendsto_def _ _ f, gbasis], + rintro ⟨B, hBl, hfBk⟩, + choose x h using hfBk, + use x, split, + { simp only [tendsto_at_top', gbasis], + rintros A ⟨i, hgiA⟩, + use i, + refine (λ j hj, hgiA $ gmon _ _ hj _), + simp only [h] }, + { simp only [tendsto_at_top', (∘), not_forall, not_exists], + use [B, hBl], + intro i, use [i, (le_refl _)], + apply (h i).right }, +end + +lemma tendsto_of_seq_tendsto {f : α → β} {k : filter α} {l : filter β} + (hcb : k.is_countably_generated) : + (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) → tendsto f k l := +hcb.tendsto_iff_seq_tendsto.2 + +end is_countably_generated + +-- TODO : prove this for a encodable type +lemma is_countably_generated_at_top_finset_nat : (at_top : filter $ finset ℕ).is_countably_generated := +begin + apply is_countably_generated_of_seq, + use λ N, Ici (finset.range N), + apply eq_infi_of_mem_sets_iff_exists_mem, + assume s, + rw mem_at_top_sets, + refine ⟨_, λ ⟨N, hN⟩, ⟨finset.range N, hN⟩⟩, + rintros ⟨t, ht⟩, + rcases mem_at_top_sets.1 (tendsto_finset_range (mem_at_top t)) with ⟨N, hN⟩, + simp only [preimage, mem_set_of_eq] at hN, + exact ⟨N, mem_principal_sets.2 $ λ t' ht', ht t' $ le_trans (hN _ $ le_refl N) ht'⟩ +end end filter diff --git a/src/order/filter/basic.lean b/src/order/filter/basic.lean index 46df0c3b8b266..32e355c070a14 100644 --- a/src/order/filter/basic.lean +++ b/src/order/filter/basic.lean @@ -10,52 +10,77 @@ import data.set.finite ## Main definitions -* `filter` : filter on a set; +* `filter` : filters on a set; * `at_top`, `at_bot`, `cofinite`, `principal` : specific filters; -* `map`, `comap`, `join` : operations on filters; -* `filter_upwards [h₁, ..., hₙ]` : takes a list of proofs `hᵢ : sᵢ ∈ f`, and replaces a goal `s ∈ f` - with `∀ x, x ∈ s₁ → ... → x ∈ sₙ → x ∈ s`; +* `map`, `comap`, `prod` : operations on filters; +* `tendsto` : limit with respect to filters; * `eventually` : `f.eventually p` means `{x | p x} ∈ f`; * `frequently` : `f.frequently p` means `{x | ¬p x} ∉ f`. +* `filter_upwards [h₁, ..., hₙ]` : takes a list of proofs `hᵢ : sᵢ ∈ f`, and replaces a goal `s ∈ f` + with `∀ x, x ∈ s₁ → ... → x ∈ sₙ → x ∈ s`; + +Filters on a type `X` are sets of sets of `X` satisfying three conditions. They are mostly used to +abstract two related kinds of ideas: +* *limits*, including finite or infinite limits of sequences, finite or infinite limits of functions + at a point or at infinity, etc... +* *things happening eventually*, including things happening for large enough `n : ℕ`, or near enough + a point `x`, or for close enough pairs of points, or things happening almost everywhere in the + sense of measure theory. Dually, filters can also express the idea of *things happening often*: + for arbitrarily large `n`, or at a point in any neighborhood of given a point etc... + +In this file, we define the type `filter X` of filters on `X`, and endow it with a complete lattice +structure. This structure is lifted from the lattice structure on `set (set X)` using the Galois +insertion which maps a filter to its elements in one direction, and an arbitrary set of sets to +the smallest filter containing it in the other direction. +We also prove `filter` is a monadic functor, with a push-forward operation +`filter.map` and a pull-back operation `filter.comap` that form a Galois connections for the +order on filters. +Finally we describe a product operation `filter X → filter Y → filter (X × Y)`. + +The examples of filters appearing in the description of the two motivating ideas are: +* `(at_top : filter ℕ)` : made of sets of `ℕ` containing `{n | n ≥ N}` for some `N` +* `𝓝 x` : made of neighborhoods of `x` in a topological space (defined in topology.basic) +* `𝓤 X` : made of entourages of a uniform space (those space are generalizations of metric spaces + defined in topology.uniform_space.basic) +* `μ.a_e` : made of sets whose complement has zero measure with respect to `μ` (defined in + measure_theory.measure_space) + +The general notion of limit of a map with respect to filters on the source and target types +is `filter.tendsto`. It is defined in terms of the order and the push-forward operation. +The predicate "happening eventually" is `filter.eventually`, and "happening often" is +`filter.frequently`, whose definitions are immediate after `filter` is defined (but they come +rather late in this file in order to immediately relate them to the lattice structure). + +For instance, anticipating on topology.basic, the statement: "if a sequence `u` converges to +some `x` and `u n` belongs to a set `M` for `n` large enough then `x` is in the closure of +`M`" is formalized as: `tendsto u at_top (𝓝 x) → (∀ᶠ n in at_top, u n ∈ M) → x ∈ closure M`, +which is a special case of `mem_closure_of_tendsto` from topology.basic. ## Notations * `∀ᶠ x in f, p x` : `f.eventually p`; * `∃ᶠ x in f, p x` : `f.frequently p`. * `f ×ᶠ g` : `filter.prod f g`, localized in `filter`. + +## References + +* [N. Bourbaki, *General Topology*][bourbaki1966] + +Important note: Bourbaki requires that a filter on `X` cannot contain all sets of `X`, which +we do *not* require. This gives `filter X` better formal properties, in particular a bottom element +`⊥` for its lattice structure, at the cost of including the assumption +`f ≠ ⊥` in a number of lemmas and definitions. -/ + open set universes u v w x y open_locale classical -section order -variables {α : Type u} (r : α → α → Prop) -local infix ` ≼ ` : 50 := r - -lemma directed_on_Union {r} {ι : Sort v} {f : ι → set α} (hd : directed (⊆) f) - (h : ∀x, directed_on r (f x)) : directed_on r (⋃x, f x) := -by simp only [directed_on, exists_prop, mem_Union, exists_imp_distrib]; exact -assume a₁ b₁ fb₁ a₂ b₂ fb₂, -let ⟨z, zb₁, zb₂⟩ := hd b₁ b₂, - ⟨x, xf, xa₁, xa₂⟩ := h z a₁ (zb₁ fb₁) a₂ (zb₂ fb₂) in -⟨x, ⟨z, xf⟩, xa₁, xa₂⟩ - -end order - -theorem directed_of_chain {α β r} [is_refl β r] {f : α → β} {c : set α} - (h : zorn.chain (f ⁻¹'o r) c) : - directed r (λx:{a:α // a ∈ c}, f (x.val)) := -assume ⟨a, ha⟩ ⟨b, hb⟩, classical.by_cases - (assume : a = b, by simp only [this, exists_prop, and_self, subtype.exists]; - exact ⟨b, hb, refl _⟩) - (assume : a ≠ b, (h a ha b hb this).elim - (λ h : r (f a) (f b), ⟨⟨b, hb⟩, h, refl _⟩) - (λ h : r (f b) (f a), ⟨⟨a, ha⟩, refl _, h⟩)) - /-- A filter `F` on a type `α` is a collection of sets of `α` which contains the whole `α`, -is upwards-closed, and is stable under intersection, -/ +is upwards-closed, and is stable under intersection. We do not forbid this collection to be +all sets of `α`. -/ structure filter (α : Type*) := (sets : set (set α)) (univ_sets : set.univ ∈ sets) @@ -110,6 +135,10 @@ finite.induction_on hf have h₂ : (⋂x∈is, s x) ∈ f, from hi $ assume a ha, hs _ $ by simp only [ha, mem_insert_iff, or_true], by simp [inter_mem_sets h₁ h₂]) +lemma sInter_mem_sets_of_finite {s : set (set α)} (hfin : finite s) (h_in : ∀ U ∈ s, U ∈ f) : + ⋂₀ s ∈ f := +by { rw sInter_eq_bInter, exact Inter_mem_sets hfin h_in } + lemma Inter_mem_sets_of_fintype {β : Type v} {s : β → set α} [fintype β] (h : ∀i, s i ∈ f) : (⋂i, s i) ∈ f := by simpa using Inter_mem_sets finite_univ (λi hi, h i) @@ -211,6 +240,37 @@ iff.intro (assume x y _ hxy hx, mem_sets_of_superset hx hxy) (assume x y _ _ hx hy, inter_mem_sets hx hy)) + +lemma mem_generate_iff (s : set $ set α) {U : set α} : U ∈ generate s ↔ ∃ t ⊆ s, finite t ∧ ⋂₀ t ⊆ U := +begin + split ; intro h, + { induction h with V V_in V W V_in hVW hV V W V_in W_in hV hW, + { use {V}, + simp [V_in] }, + { use ∅, + simp [subset.refl, univ] }, + { rcases hV with ⟨t, hts, htfin, hinter⟩, + exact ⟨t, hts, htfin, subset.trans hinter hVW⟩ }, + { rcases hV with ⟨t, hts, htfin, htinter⟩, + rcases hW with ⟨z, hzs, hzfin, hzinter⟩, + refine ⟨t ∪ z, union_subset hts hzs, finite_union htfin hzfin, _⟩, + rw sInter_union, + exact inter_subset_inter htinter hzinter } }, + { rcases h with ⟨t, ts, tfin, h⟩, + apply generate_sets.superset _ h, + revert ts, + apply finite.induction_on tfin, + { intro h, + rw sInter_empty, + exact generate_sets.univ }, + { intros V r hV rfin hinter h, + cases insert_subset.mp h with V_in r_sub, + rw [insert_eq V r, sInter_union], + apply generate_sets.inter _ (hinter r_sub), + rw sInter_singleton, + exact generate_sets.basic V_in } }, +end + /-- `mk_of_closure s hs` constructs a filter on `α` whose elements set is exactly `s : set (set α)`, provided one gives the assumption `hs : (generate s).sets = s`. -/ protected def mk_of_closure (s : set (set α)) (hs : (generate s).sets = s) : filter α := @@ -340,6 +400,32 @@ iff.rfl x ∈ supr f ↔ (∀i, x ∈ f i) := by simp only [supr_sets_eq, iff_self, mem_Inter] +lemma infi_eq_generate (s : ι → filter α) : infi s = generate (⋃ i, (s i).sets) := +show generate _ = generate _, from congr_arg _ supr_range + +lemma mem_infi_iff {ι} {s : ι → filter α} {U : set α} : (U ∈ ⨅ i, s i) ↔ + ∃ I : set ι, finite I ∧ ∃ V : {i | i ∈ I} → set α, (∀ i, V i ∈ s i) ∧ (⋂ i, V i) ⊆ U := +begin + rw [infi_eq_generate, mem_generate_iff], + split, + { rintro ⟨t, tsub, tfin, tinter⟩, + rcases eq_finite_Union_of_finite_subset_Union tfin tsub with ⟨I, Ifin, σ, σfin, σsub, rfl⟩, + rw sInter_Union at tinter, + let V := λ i, ⋂₀ σ i, + have V_in : ∀ i, V i ∈ s i, + { rintro ⟨i, i_in⟩, + apply sInter_mem_sets_of_finite (σfin _), + apply σsub }, + exact ⟨I, Ifin, V, V_in, tinter⟩ }, + { rintro ⟨I, Ifin, V, V_in, h⟩, + refine ⟨range V, _, _, h⟩, + { rintro _ ⟨i, rfl⟩, + rw mem_Union, + use [i, V_in i] }, + { haveI : fintype {i : ι | i ∈ I} := finite.fintype Ifin, + exact finite_range _ } }, +end + @[simp] lemma le_principal_iff {s : set α} {f : filter α} : f ≤ principal s ↔ s ∈ f := show (∀{t}, s ⊆ t → t ∈ f) ↔ s ∈ f, from ⟨assume h, h (subset.refl s), assume hs t ht, mem_sets_of_superset hs ht⟩ @@ -355,6 +441,12 @@ by simp only [le_antisymm_iff, le_principal_iff, mem_principal_sets]; refl @[simp] lemma join_principal_eq_Sup {s : set (filter α)} : join (principal s) = Sup s := rfl +lemma principal_univ : principal (univ : set α) = ⊤ := +top_unique $ by simp only [le_principal_iff, mem_top_sets, eq_self_iff_true] + +lemma principal_empty : principal (∅ : set α) = ⊥ := +bot_unique $ assume s _, empty_subset _ + /-! ### Lattice equations -/ lemma empty_in_sets_eq_bot {f : filter α} : ∅ ∈ f ↔ f = ⊥ := @@ -532,6 +624,118 @@ begin exact ⟨p a, hpa, (s.inf p), ⟨⟨p, hp, le_refl _⟩, ht⟩⟩ } end +/-- If `f : ι → filter α` is directed, `ι` is not empty, and `∀ i, f i ≠ ⊥`, then `infi f ≠ ⊥`. +See also `infi_ne_bot_of_directed` for a version assuming `nonempty α` instead of `nonempty ι`. -/ +lemma infi_ne_bot_of_directed' {f : ι → filter α} (hn : nonempty ι) + (hd : directed (≥) f) (hb : ∀i, f i ≠ ⊥) : (infi f) ≠ ⊥ := +begin + intro h, + have he: ∅ ∈ (infi f), from h.symm ▸ (mem_bot_sets : ∅ ∈ (⊥ : filter α)), + obtain ⟨i, hi⟩ : ∃i, ∅ ∈ f i, + from (mem_infi hd hn ∅).1 he, + exact hb i (empty_in_sets_eq_bot.1 hi) +end + +/-- If `f : ι → filter α` is directed, `α` is not empty, and `∀ i, f i ≠ ⊥`, then `infi f ≠ ⊥`. +See also `infi_ne_bot_of_directed'` for a version assuming `nonempty ι` instead of `nonempty α`. -/ +lemma infi_ne_bot_of_directed {f : ι → filter α} + (hn : nonempty α) (hd : directed (≥) f) (hb : ∀i, f i ≠ ⊥) : (infi f) ≠ ⊥ := +if hι : nonempty ι then infi_ne_bot_of_directed' hι hd hb else +assume h : infi f = ⊥, +have univ ⊆ (∅ : set α), +begin + rw [←principal_mono, principal_univ, principal_empty, ←h], + exact (le_infi $ assume i, false.elim $ hι ⟨i⟩) +end, +let ⟨x⟩ := hn in this (mem_univ x) + +lemma infi_ne_bot_iff_of_directed' {f : ι → filter α} + (hn : nonempty ι) (hd : directed (≥) f) : (infi f) ≠ ⊥ ↔ (∀i, f i ≠ ⊥) := +⟨assume ne_bot i, ne_bot_of_le_ne_bot ne_bot (infi_le _ i), + infi_ne_bot_of_directed' hn hd⟩ + +lemma infi_ne_bot_iff_of_directed {f : ι → filter α} + (hn : nonempty α) (hd : directed (≥) f) : (infi f) ≠ ⊥ ↔ (∀i, f i ≠ ⊥) := +⟨assume ne_bot i, ne_bot_of_le_ne_bot ne_bot (infi_le _ i), + infi_ne_bot_of_directed hn hd⟩ + +lemma mem_infi_sets {f : ι → filter α} (i : ι) : ∀{s}, s ∈ f i → s ∈ ⨅i, f i := +show (⨅i, f i) ≤ f i, from infi_le _ _ + +@[elab_as_eliminator] +lemma infi_sets_induct {f : ι → filter α} {s : set α} (hs : s ∈ infi f) {p : set α → Prop} + (uni : p univ) + (ins : ∀{i s₁ s₂}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)) + (upw : ∀{s₁ s₂}, s₁ ⊆ s₂ → p s₁ → p s₂) : p s := +begin + rw [mem_infi_finite] at hs, + simp only [mem_Union, (finset.inf_eq_infi _ _).symm] at hs, + rcases hs with ⟨is, his⟩, + revert s, + refine finset.induction_on is _ _, + { assume s hs, rwa [mem_top_sets.1 hs] }, + { rintros ⟨i⟩ js his ih s hs, + rw [finset.inf_insert, mem_inf_sets] at hs, + rcases hs with ⟨s₁, hs₁, s₂, hs₂, hs⟩, + exact upw hs (ins hs₁ (ih hs₂)) } +end + +/- principal equations -/ + +@[simp] lemma inf_principal {s t : set α} : principal s ⊓ principal t = principal (s ∩ t) := +le_antisymm + (by simp; exact ⟨s, subset.refl s, t, subset.refl t, by simp⟩) + (by simp [le_inf_iff, inter_subset_left, inter_subset_right]) + +@[simp] lemma sup_principal {s t : set α} : principal s ⊔ principal t = principal (s ∪ t) := +filter_eq $ set.ext $ + by simp only [union_subset_iff, union_subset_iff, mem_sup_sets, forall_const, iff_self, mem_principal_sets] + +@[simp] lemma supr_principal {ι : Sort w} {s : ι → set α} : (⨆x, principal (s x)) = principal (⋃i, s i) := +filter_eq $ set.ext $ assume x, by simp only [supr_sets_eq, mem_principal_sets, mem_Inter]; +exact (@supr_le_iff (set α) _ _ _ _).symm + +@[simp] lemma principal_eq_bot_iff {s : set α} : principal s = ⊥ ↔ s = ∅ := +empty_in_sets_eq_bot.symm.trans $ mem_principal_sets.trans subset_empty_iff + +lemma principal_ne_bot_iff {s : set α} : principal s ≠ ⊥ ↔ s.nonempty := +(not_congr principal_eq_bot_iff).trans ne_empty_iff_nonempty + +lemma inf_principal_eq_bot {f : filter α} {s : set α} (hs : -s ∈ f) : f ⊓ principal s = ⊥ := +empty_in_sets_eq_bot.mp ⟨_, hs, s, mem_principal_self s, assume x ⟨h₁, h₂⟩, h₁ h₂⟩ + +theorem mem_inf_principal (f : filter α) (s t : set α) : + s ∈ f ⊓ principal t ↔ {x | x ∈ t → x ∈ s} ∈ f := +begin + simp only [mem_inf_sets, mem_principal_sets, exists_prop], split, + { rintros ⟨u, ul, v, tsubv, uvinter⟩, + apply filter.mem_sets_of_superset ul, + intros x xu xt, exact uvinter ⟨xu, tsubv xt⟩ }, + intro h, refine ⟨_, h, t, set.subset.refl t, _⟩, + rintros x ⟨hx, xt⟩, + exact hx xt +end + +@[simp] lemma infi_principal_finset {ι : Type w} (s : finset ι) (f : ι → set α) : + (⨅i∈s, principal (f i)) = principal (⋂i∈s, f i) := +begin + ext t, + simp [mem_infi_sets_finset], + split, + { rintros ⟨p, hp, ht⟩, + calc (⋂ (i : ι) (H : i ∈ s), f i) ≤ (⋂ (i : ι) (H : i ∈ s), p i) : + infi_le_infi (λi, infi_le_infi (λhi, mem_principal_sets.1 (hp i hi))) + ... ≤ t : ht }, + { assume h, + exact ⟨f, λi hi, subset.refl _, h⟩ } +end + +@[simp] lemma infi_principal_fintype {ι : Type w} [fintype ι] (f : ι → set α) : + (⨅i, principal (f i)) = principal (⋂i, f i) := +by simpa using infi_principal_finset finset.univ f + +end lattice + /-! ### Eventually -/ /-- `f.eventually p` or `∀ᶠ x in f, p x` mean that `{x | p x} ∈ f`. E.g., `∀ᶠ x in at_top, p x` @@ -777,67 +981,7 @@ lemma frequently_supr {p : α → Prop} {fs : β → filter α} : (∃ᶠ x in (⨆ b, fs b), p x) ↔ (∃ b, ∃ᶠ x in fs b, p x) := by simp [filter.frequently, -not_eventually, not_forall] -/- principal equations -/ - -@[simp] lemma inf_principal {s t : set α} : principal s ⊓ principal t = principal (s ∩ t) := -le_antisymm - (by simp; exact ⟨s, subset.refl s, t, subset.refl t, by simp⟩) - (by simp [le_inf_iff, inter_subset_left, inter_subset_right]) - -@[simp] lemma sup_principal {s t : set α} : principal s ⊔ principal t = principal (s ∪ t) := -filter_eq $ set.ext $ - by simp only [union_subset_iff, union_subset_iff, mem_sup_sets, forall_const, iff_self, mem_principal_sets] - -@[simp] lemma supr_principal {ι : Sort w} {s : ι → set α} : (⨆x, principal (s x)) = principal (⋃i, s i) := -filter_eq $ set.ext $ assume x, by simp only [supr_sets_eq, mem_principal_sets, mem_Inter]; -exact (@supr_le_iff (set α) _ _ _ _).symm - -lemma principal_univ : principal (univ : set α) = ⊤ := -top_unique $ by simp only [le_principal_iff, mem_top_sets, eq_self_iff_true] - -lemma principal_empty : principal (∅ : set α) = ⊥ := -bot_unique $ assume s _, empty_subset _ - -@[simp] lemma principal_eq_bot_iff {s : set α} : principal s = ⊥ ↔ s = ∅ := -empty_in_sets_eq_bot.symm.trans $ mem_principal_sets.trans subset_empty_iff - -lemma principal_ne_bot_iff {s : set α} : principal s ≠ ⊥ ↔ s.nonempty := -(not_congr principal_eq_bot_iff).trans ne_empty_iff_nonempty - -lemma inf_principal_eq_bot {f : filter α} {s : set α} (hs : -s ∈ f) : f ⊓ principal s = ⊥ := -empty_in_sets_eq_bot.mp ⟨_, hs, s, mem_principal_self s, assume x ⟨h₁, h₂⟩, h₁ h₂⟩ - -theorem mem_inf_principal (f : filter α) (s t : set α) : - s ∈ f ⊓ principal t ↔ { x | x ∈ t → x ∈ s } ∈ f := -begin - simp only [mem_inf_sets, mem_principal_sets, exists_prop], split, - { rintros ⟨u, ul, v, tsubv, uvinter⟩, - apply filter.mem_sets_of_superset ul, - intros x xu xt, exact uvinter ⟨xu, tsubv xt⟩ }, - intro h, refine ⟨_, h, t, set.subset.refl t, _⟩, - rintros x ⟨hx, xt⟩, - exact hx xt -end - -@[simp] lemma infi_principal_finset {ι : Type w} (s : finset ι) (f : ι → set α) : - (⨅i∈s, principal (f i)) = principal (⋂i∈s, f i) := -begin - ext t, - simp [mem_infi_sets_finset], - split, - { rintros ⟨p, hp, ht⟩, - calc (⋂ (i : ι) (H : i ∈ s), f i) ≤ (⋂ (i : ι) (H : i ∈ s), p i) : - infi_le_infi (λi, infi_le_infi (λhi, mem_principal_sets.1 (hp i hi))) - ... ≤ t : ht }, - { assume h, - exact ⟨f, λi hi, subset.refl _, h⟩ } -end - -@[simp] lemma infi_principal_fintype {ι : Type w} [fintype ι] (f : ι → set α) : - (⨅i, principal (f i)) = principal (⋂i, f i) := -by simpa using infi_principal_finset finset.univ f - -end lattice +/-! ### Push-forwards, pull-backs, and the monad structure -/ section map @@ -918,25 +1062,6 @@ end end comap -/-- The cofinite filter is the filter of subsets whose complements are finite. -/ -def cofinite : filter α := -{ sets := {s | finite (- s)}, - univ_sets := by simp only [compl_univ, finite_empty, mem_set_of_eq], - sets_of_superset := assume s t (hs : finite (-s)) (st: s ⊆ t), - finite_subset hs $ compl_subset_compl.2 st, - inter_sets := assume s t (hs : finite (-s)) (ht : finite (-t)), - by simp only [compl_inter, finite_union, ht, hs, mem_set_of_eq] } - -@[simp] lemma mem_cofinite {s : set α} : s ∈ (@cofinite α) ↔ finite (-s) := iff.rfl - -lemma cofinite_ne_bot [infinite α] : @cofinite α ≠ ⊥ := -mt empty_in_sets_eq_bot.mpr $ by { simp only [mem_cofinite, compl_empty], exact infinite_univ } - -lemma frequently_cofinite_iff_infinite {p : α → Prop} : - (∃ᶠ x in cofinite, p x) ↔ set.infinite {x | p x} := -by simp only [filter.frequently, filter.eventually, mem_cofinite, compl_set_of, not_not, - set.infinite] - /-- The monadic bind operation on filter is defined the usual way in terms of `map` and `join`. Unfortunately, this `bind` does not result in the expected applicative. See `filter.seq` for the @@ -1432,63 +1557,46 @@ show join (map f (principal s)) = (⨆x ∈ s, f x), end bind -/-- If `f : ι → filter α` is derected, `ι` is not empty, and `∀ i, f i ≠ ⊥`, then `infi f ≠ ⊥`. -See also `infi_ne_bot_of_directed` for a version assuming `nonempty α` instead of `nonempty ι`. -/ -lemma infi_ne_bot_of_directed' {f : ι → filter α} (hn : nonempty ι) - (hd : directed (≥) f) (hb : ∀i, f i ≠ ⊥) : (infi f) ≠ ⊥ := -begin - intro h, - have he: ∅ ∈ (infi f), from h.symm ▸ (mem_bot_sets : ∅ ∈ (⊥ : filter α)), - obtain ⟨i, hi⟩ : ∃i, ∅ ∈ f i, - from (mem_infi hd hn ∅).1 he, - exact hb i (empty_in_sets_eq_bot.1 hi) -end +section list_traverse +/- This is a separate section in order to open `list`, but mostly because of universe + equality requirements in `traverse` -/ -/-- If `f : ι → filter α` is derected, `α` is not empty, and `∀ i, f i ≠ ⊥`, then `infi f ≠ ⊥`. -See also `infi_ne_bot_of_directed'` for a version assuming `nonempty ι` instead of `nonempty α`. -/ -lemma infi_ne_bot_of_directed {f : ι → filter α} - (hn : nonempty α) (hd : directed (≥) f) (hb : ∀i, f i ≠ ⊥) : (infi f) ≠ ⊥ := -if hι : nonempty ι then infi_ne_bot_of_directed' hι hd hb else -assume h : infi f = ⊥, -have univ ⊆ (∅ : set α), -begin - rw [←principal_mono, principal_univ, principal_empty, ←h], - exact (le_infi $ assume i, false.elim $ hι ⟨i⟩) -end, -let ⟨x⟩ := hn in this (mem_univ x) +open list -lemma infi_ne_bot_iff_of_directed' {f : ι → filter α} - (hn : nonempty ι) (hd : directed (≥) f) : (infi f) ≠ ⊥ ↔ (∀i, f i ≠ ⊥) := -⟨assume ne_bot i, ne_bot_of_le_ne_bot ne_bot (infi_le _ i), - infi_ne_bot_of_directed' hn hd⟩ +lemma sequence_mono : + ∀(as bs : list (filter α)), forall₂ (≤) as bs → sequence as ≤ sequence bs +| [] [] forall₂.nil := le_refl _ +| (a::as) (b::bs) (forall₂.cons h hs) := seq_mono (map_mono h) (sequence_mono as bs hs) -lemma infi_ne_bot_iff_of_directed {f : ι → filter α} - (hn : nonempty α) (hd : directed (≥) f) : (infi f) ≠ ⊥ ↔ (∀i, f i ≠ ⊥) := -⟨assume ne_bot i, ne_bot_of_le_ne_bot ne_bot (infi_le _ i), - infi_ne_bot_of_directed hn hd⟩ +variables {α' β' γ' : Type u} {f : β' → filter α'} {s : γ' → set α'} -lemma mem_infi_sets {f : ι → filter α} (i : ι) : ∀{s}, s ∈ f i → s ∈ ⨅i, f i := -show (⨅i, f i) ≤ f i, from infi_le _ _ +lemma mem_traverse_sets : + ∀(fs : list β') (us : list γ'), + forall₂ (λb c, s c ∈ f b) fs us → traverse s us ∈ traverse f fs +| [] [] forall₂.nil := mem_pure_sets.2 $ mem_singleton _ +| (f::fs) (u::us) (forall₂.cons h hs) := seq_mem_seq_sets (image_mem_map h) (mem_traverse_sets fs us hs) -@[elab_as_eliminator] -lemma infi_sets_induct {f : ι → filter α} {s : set α} (hs : s ∈ infi f) {p : set α → Prop} - (uni : p univ) - (ins : ∀{i s₁ s₂}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)) - (upw : ∀{s₁ s₂}, s₁ ⊆ s₂ → p s₁ → p s₂) : p s := +lemma mem_traverse_sets_iff (fs : list β') (t : set (list α')) : + t ∈ traverse f fs ↔ + (∃us:list (set α'), forall₂ (λb (s : set α'), s ∈ f b) fs us ∧ sequence us ⊆ t) := begin - rw [mem_infi_finite] at hs, - simp only [mem_Union, (finset.inf_eq_infi _ _).symm] at hs, - rcases hs with ⟨is, his⟩, - revert s, - refine finset.induction_on is _ _, - { assume s hs, rwa [mem_top_sets.1 hs] }, - { rintros ⟨i⟩ js his ih s hs, - rw [finset.inf_insert, mem_inf_sets] at hs, - rcases hs with ⟨s₁, hs₁, s₂, hs₂, hs⟩, - exact upw hs (ins hs₁ (ih hs₂)) } + split, + { induction fs generalizing t, + case nil { simp only [sequence, mem_pure_sets, imp_self, forall₂_nil_left_iff, + exists_eq_left, set.pure_def, singleton_subset_iff, traverse_nil] }, + case cons : b fs ih t { + assume ht, + rcases mem_seq_sets_iff.1 ht with ⟨u, hu, v, hv, ht⟩, + rcases mem_map_sets_iff.1 hu with ⟨w, hw, hwu⟩, + rcases ih v hv with ⟨us, hus, hu⟩, + exact ⟨w :: us, forall₂.cons hw hus, subset.trans (set.seq_mono hwu hu) ht⟩ } }, + { rintros ⟨us, hus, hs⟩, + exact mem_sets_of_superset (mem_traverse_sets _ _ hus) hs } end -/- tendsto -/ +end list_traverse + +/-! ### Limits -/ /-- `tendsto` is the generic "limit of a function" predicate. `tendsto f l₁ l₂` asserts that for every `l₂` neighborhood `a`, @@ -1641,6 +1749,7 @@ begin rw if_neg h, exact hp₁ h end +/-! ### Products of filters -/ section prod variables {s : set α} {t : set β} {f : filter α} {g : filter β} @@ -1791,7 +1900,7 @@ by simp only [tendsto_def, mem_prod_iff, prod_sub_preimage_iff, exists_prop, iff end prod -/- at_top and at_bot -/ +/-! ### at_top and at_bot filters on preorded sets, monoids and groups. -/ /-- `at_top` is the filter representing the limit `→ ∞` on an ordered set. It is generated by the collection of up-sets `{b | a ≤ b}`. @@ -1879,6 +1988,11 @@ lemma tendsto_at_top_mono [preorder β] (l : filter α) : monotone (λ f : α → β, tendsto f l at_top) := λ f₁ f₂ h, tendsto_at_top_mono' l $ univ_mem_sets' h +@[nolint ge_or_gt] -- see Note [nolint_ge] +lemma map_at_top_inf_ne_bot_iff [semilattice_sup α] [nonempty α] {F : filter β} {u : α → β} : + (map u at_top) ⊓ F ≠ ⊥ ↔ ∀ U ∈ F, ∀ N, ∃ n ≥ N, u n ∈ U := +by simp_rw [inf_ne_bot_iff_frequently_right, frequently_map, frequently_at_top] ; trivial + section ordered_add_monoid variables [ordered_cancel_add_comm_monoid β] (l : filter α) {f g : α → β} @@ -2083,7 +2197,51 @@ map_at_top_eq_of_gc (λb, b * k + (k - 1)) 1 calc b = (b * k) / k : by rw [nat.mul_div_cancel b hk] ... ≤ (b * k + (k - 1)) / k : nat.div_le_div_right $ nat.le_add_right _ _) -/- ultrafilter -/ +/-! ### The cofinite filter -/ + +/-- The cofinite filter is the filter of subsets whose complements are finite. -/ +def cofinite : filter α := +{ sets := {s | finite (- s)}, + univ_sets := by simp only [compl_univ, finite_empty, mem_set_of_eq], + sets_of_superset := assume s t (hs : finite (-s)) (st: s ⊆ t), + finite_subset hs $ compl_subset_compl.2 st, + inter_sets := assume s t (hs : finite (-s)) (ht : finite (-t)), + by simp only [compl_inter, finite_union, ht, hs, mem_set_of_eq] } + +@[simp] lemma mem_cofinite {s : set α} : s ∈ (@cofinite α) ↔ finite (-s) := iff.rfl + +lemma cofinite_ne_bot [infinite α] : @cofinite α ≠ ⊥ := +mt empty_in_sets_eq_bot.mpr $ by { simp only [mem_cofinite, compl_empty], exact infinite_univ } + +lemma frequently_cofinite_iff_infinite {p : α → Prop} : + (∃ᶠ x in cofinite, p x) ↔ set.infinite {x | p x} := +by simp only [filter.frequently, filter.eventually, mem_cofinite, compl_set_of, not_not, + set.infinite] + +lemma set.infinite_iff_frequently_cofinite {α : Type u} {s : set α} : + set.infinite s ↔ (∃ᶠ x in cofinite, x ∈ s) := +frequently_cofinite_iff_infinite.symm + +/-- For natural numbers the filters `cofinite` and `at_top` coincide. -/ +lemma nat.cofinite_eq_at_top : @cofinite ℕ = at_top := +begin + ext s, + simp only [mem_cofinite, mem_at_top_sets], + split, + { assume hs, + use (hs.to_finset.sup id) + 1, + assume b hb, + by_contradiction hbs, + have := hs.to_finset.subset_range_sup_succ (finite.mem_to_finset.2 hbs), + exact not_lt_of_le hb (finset.mem_range.1 this) }, + { rintros ⟨N, hN⟩, + apply finite_subset (finite_lt_nat N), + assume n hn, + change n < N, + exact lt_of_not_ge (λ hn', hn $ hN n hn') } +end + +/-! ### Ultrafilters -/ section ultrafilter open zorn @@ -2314,63 +2472,3 @@ lemma exists_ultrafilter_iff (f : filter α) : (∃ (u : ultrafilter α), u.val end ultrafilter end filter - -namespace filter -variables {α β γ : Type u} {f : β → filter α} {s : γ → set α} -open list - -lemma mem_traverse_sets : - ∀(fs : list β) (us : list γ), - forall₂ (λb c, s c ∈ f b) fs us → traverse s us ∈ traverse f fs -| [] [] forall₂.nil := mem_pure_sets.2 $ mem_singleton _ -| (f::fs) (u::us) (forall₂.cons h hs) := seq_mem_seq_sets (image_mem_map h) (mem_traverse_sets fs us hs) - -lemma mem_traverse_sets_iff (fs : list β) (t : set (list α)) : - t ∈ traverse f fs ↔ - (∃us:list (set α), forall₂ (λb (s : set α), s ∈ f b) fs us ∧ sequence us ⊆ t) := -begin - split, - { induction fs generalizing t, - case nil { simp only [sequence, mem_pure_sets, imp_self, forall₂_nil_left_iff, - exists_eq_left, set.pure_def, singleton_subset_iff, traverse_nil] }, - case cons : b fs ih t { - assume ht, - rcases mem_seq_sets_iff.1 ht with ⟨u, hu, v, hv, ht⟩, - rcases mem_map_sets_iff.1 hu with ⟨w, hw, hwu⟩, - rcases ih v hv with ⟨us, hus, hu⟩, - exact ⟨w :: us, forall₂.cons hw hus, subset.trans (set.seq_mono hwu hu) ht⟩ } }, - { rintros ⟨us, hus, hs⟩, - exact mem_sets_of_superset (mem_traverse_sets _ _ hus) hs } -end - -lemma sequence_mono : - ∀(as bs : list (filter α)), forall₂ (≤) as bs → sequence as ≤ sequence bs -| [] [] forall₂.nil := le_refl _ -| (a::as) (b::bs) (forall₂.cons h hs) := seq_mono (map_mono h) (sequence_mono as bs hs) - -end filter - -open filter - -lemma set.infinite_iff_frequently_cofinite {α : Type u} {s : set α} : - set.infinite s ↔ (∃ᶠ x in cofinite, x ∈ s) := -frequently_cofinite_iff_infinite.symm - -/-- For natural numbers the filters `cofinite` and `at_top` coincide. -/ -lemma nat.cofinite_eq_at_top : @cofinite ℕ = at_top := -begin - ext s, - simp only [mem_cofinite, mem_at_top_sets], - split, - { assume hs, - use (hs.to_finset.sup id) + 1, - assume b hb, - by_contradiction hbs, - have := hs.to_finset.subset_range_sup_succ (finite.mem_to_finset.2 hbs), - exact not_lt_of_le hb (finset.mem_range.1 this) }, - { rintros ⟨N, hN⟩, - apply finite_subset (finite_lt_nat N), - assume n hn, - change n < N, - exact lt_of_not_ge (λ hn', hn $ hN n hn') } -end diff --git a/src/order/zorn.lean b/src/order/zorn.lean index 82591bf9c8b72..4d2c924f2f159 100644 --- a/src/order/zorn.lean +++ b/src/order/zorn.lean @@ -287,3 +287,13 @@ theorem chain.image {α β : Type*} (r : α → α → Prop) (or.inl ∘ h _ _) (or.inr ∘ h _ _) end zorn + +theorem directed_of_chain {α β r} [is_refl β r] {f : α → β} {c : set α} + (h : zorn.chain (f ⁻¹'o r) c) : + directed r (λx:{a:α // a ∈ c}, f (x.val)) := +assume ⟨a, ha⟩ ⟨b, hb⟩, classical.by_cases + (assume : a = b, by simp only [this, exists_prop, and_self, subtype.exists]; + exact ⟨b, hb, refl _⟩) + (assume : a ≠ b, (h a ha b hb this).elim + (λ h : r (f a) (f b), ⟨⟨b, hb⟩, h, refl _⟩) + (λ h : r (f b) (f a), ⟨⟨a, ha⟩, refl _, h⟩)) diff --git a/src/topology/bases.lean b/src/topology/bases.lean index a810eb0fc81e6..6ca09b9b86e70 100644 --- a/src/topology/bases.lean +++ b/src/topology/bases.lean @@ -6,151 +6,11 @@ Authors: Johannes Hölzl, Mario Carneiro Bases of topologies. Countability axioms. -/ -import topology.constructions data.set.countable +import topology.constructions order.filter.bases open set filter classical open_locale topological_space -namespace filter -universes u v -variables {α : Type u} {β : Type v} - -/-- -A filter has a countable basis iff it is generated by a countable collection -of subsets of α. (A filter is a generated by a collection of sets iff it is -the infimum of the principal filters.) - -Note: we do not require the collection to be closed under finite intersections. --/ -def has_countable_basis (f : filter α) : Prop := -∃ s : set (set α), countable s ∧ f = ⨅ t ∈ s, principal t - -lemma has_countable_basis_of_seq (f : filter α) (x : ℕ → set α) (h : f = ⨅ i, principal (x i)) : - f.has_countable_basis := -⟨range x, countable_range _, by rwa infi_range⟩ - -lemma seq_of_has_countable_basis (f : filter α) (cblb : f.has_countable_basis) : - ∃ x : ℕ → set α, f = ⨅ i, principal (x i) := -begin - rcases cblb with ⟨B, Bcbl, gen⟩, subst gen, - cases B.eq_empty_or_nonempty with hB Bnonempty, { use λ n, set.univ, simp [principal_univ, *] }, - rw countable_iff_exists_surjective_to_subtype Bnonempty at Bcbl, - rcases Bcbl with ⟨g, gsurj⟩, - rw infi_subtype', - use (λ n, g n), apply le_antisymm; rw le_infi_iff, - { intro i, apply infi_le_of_le (g i) _, apply le_refl _ }, - { intros a, rcases gsurj a with i, apply infi_le_of_le i _, subst h, apply le_refl _ } -end - -/-- -Different characterization of countable basis. A filter has a countable basis -iff it is generated by a sequence of sets. --/ -lemma has_countable_basis_iff_seq (f : filter α) : - f.has_countable_basis ↔ - ∃ x : ℕ → set α, f = ⨅ i, principal (x i) := -⟨seq_of_has_countable_basis _, λ ⟨x, xgen⟩, has_countable_basis_of_seq _ x xgen⟩ - -lemma mono_seq_of_has_countable_basis (f : filter α) (cblb : f.has_countable_basis) : - ∃ x : ℕ → set α, (∀ i j, i ≤ j → x j ⊆ x i) ∧ f = ⨅ i, principal (x i) := -begin - rcases (seq_of_has_countable_basis f cblb) with ⟨x', hx'⟩, - let x := λ n, ⋂ m ≤ n, x' m, - use x, split, - { intros i j hij a, simp [x], intros h i' hi'i, apply h, transitivity; assumption }, - subst hx', apply le_antisymm; rw le_infi_iff; intro i, - { rw le_principal_iff, apply Inter_mem_sets (finite_le_nat _), - intros j hji, rw ← le_principal_iff, apply infi_le_of_le j _, apply le_refl _ }, - { apply infi_le_of_le i _, rw principal_mono, intro a, simp [x], intro h, apply h, refl }, -end - -/-- -Different characterization of countable basis. A filter has a countable basis -iff it is generated by a monotonically decreasing sequence of sets. --/ -lemma has_countable_basis_iff_mono_seq (f : filter α) : - f.has_countable_basis ↔ - ∃ x : ℕ → set α, (∀ i j, i ≤ j → x j ⊆ x i) ∧ f = ⨅ i, principal (x i) := -⟨mono_seq_of_has_countable_basis _, λ ⟨x, _, xgen⟩, has_countable_basis_of_seq _ x xgen⟩ - -/-- -Different characterization of countable basis. A filter has a countable basis -iff there exists a monotonically decreasing sequence of sets `x i` -such that `s ∈ f ↔ ∃ i, x i ⊆ s`. -/ -lemma has_countable_basis_iff_mono_seq' (f : filter α) : - f.has_countable_basis ↔ - ∃ x : ℕ → set α, (∀ i j, i ≤ j → x j ⊆ x i) ∧ (∀ {s}, s ∈ f ↔ ∃ i, x i ⊆ s) := -begin - refine (has_countable_basis_iff_mono_seq f).trans (exists_congr $ λ x, and_congr_right _), - intro hmono, - have : directed (≥) (λ i, principal (x i)), - from directed_of_mono _ (λ i j hij, principal_mono.2 (hmono _ _ hij)), - simp only [filter.ext_iff, mem_infi this ⟨0⟩, mem_Union, mem_principal_sets] -end - -lemma has_countable_basis.comap {l : filter β} (h : has_countable_basis l) (f : α → β) : - has_countable_basis (l.comap f) := -begin - rcases h with ⟨S, h₁, h₂⟩, - refine ⟨preimage f '' S, countable_image _ h₁, _⟩, - calc comap f l = ⨅ s ∈ S, principal (f ⁻¹' s) : by simp [h₂] - ... = ⨅ s ∈ S, ⨅ (t : set α) (H : f ⁻¹' s = t), principal t : by simp - ... = ⨅ (t : set α) (s ∈ S) (h₂ : f ⁻¹' s = t), principal t : - by { rw [infi_comm], congr' 1, ext t, rw [infi_comm] } - ... = _ : by simp [-infi_infi_eq_right, infi_and] -end - --- TODO : prove this for a encodable type -lemma has_countable_basis_at_top_finset_nat : has_countable_basis (@at_top (finset ℕ) _) := -begin - refine has_countable_basis_of_seq _ (λN, Ici (finset.range N)) (eq_infi_of_mem_sets_iff_exists_mem _), - assume s, - rw mem_at_top_sets, - refine ⟨_, λ ⟨N, hN⟩, ⟨finset.range N, hN⟩⟩, - rintros ⟨t, ht⟩, - rcases mem_at_top_sets.1 (tendsto_finset_range (mem_at_top t)) with ⟨N, hN⟩, - simp only [preimage, mem_set_of_eq] at hN, - exact ⟨N, mem_principal_sets.2 $ λ t' ht', ht t' $ le_trans (hN _ $ le_refl N) ht'⟩ -end - -lemma has_countable_basis.tendsto_iff_seq_tendsto {f : α → β} {k : filter α} {l : filter β} - (hcb : k.has_countable_basis) : - tendsto f k l ↔ (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) := -suffices (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) → tendsto f k l, - from ⟨by intros; apply tendsto.comp; assumption, by assumption⟩, -begin - rw filter.has_countable_basis_iff_mono_seq at hcb, - rcases hcb with ⟨g, gmon, gbasis⟩, - have gbasis : ∀ A, A ∈ k ↔ ∃ i, g i ⊆ A, - { intro A, - subst gbasis, - rw mem_infi, - { simp only [set.mem_Union, iff_self, filter.mem_principal_sets] }, - { exact directed_of_mono _ (λ i j h, principal_mono.mpr $ gmon _ _ h) }, - { apply_instance } }, - classical, contrapose, - simp only [not_forall, not_imp, not_exists, subset_def, @tendsto_def _ _ f, gbasis], - rintro ⟨B, hBl, hfBk⟩, - choose x h using hfBk, - use x, split, - { simp only [tendsto_at_top', gbasis], - rintros A ⟨i, hgiA⟩, - use i, - refine (λ j hj, hgiA $ gmon _ _ hj _), - simp only [h] }, - { simp only [tendsto_at_top', (∘), not_forall, not_exists], - use [B, hBl], - intro i, use [i, (le_refl _)], - apply (h i).right }, -end - -lemma has_countable_basis.tendsto_of_seq_tendsto {f : α → β} {k : filter α} {l : filter β} - (hcb : k.has_countable_basis) : - (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) → tendsto f k l := -hcb.tendsto_iff_seq_tendsto.2 - -end filter - namespace topological_space /- countability axioms @@ -255,7 +115,7 @@ class separable_space : Prop := /-- A first-countable space is one in which every point has a countable neighborhood basis. -/ class first_countable_topology : Prop := -(nhds_generated_countable : ∀a:α, (𝓝 a).has_countable_basis) +(nhds_generated_countable : ∀a:α, (𝓝 a).is_countably_generated) /-- A second-countable space is one with a countable basis. -/ class second_countable_topology : Prop := @@ -265,8 +125,11 @@ class second_countable_topology : Prop := instance second_countable_topology.to_first_countable_topology [second_countable_topology α] : first_countable_topology α := let ⟨b, hb, eq⟩ := second_countable_topology.is_open_generated_countable α in -⟨assume a, ⟨{s | a ∈ s ∧ s ∈ b}, - countable_subset (assume x ⟨_, hx⟩, hx) hb, by rw [eq, nhds_generate_from]⟩⟩ +⟨begin + intros, + rw [eq, nhds_generate_from], + exact is_countably_generated_binfi_principal (countable_subset (assume x ⟨_, hx⟩, hx) hb), + end⟩ lemma second_countable_topology_induced (β) [t : topological_space β] [second_countable_topology β] (f : α → β) : diff --git a/src/topology/basic.lean b/src/topology/basic.lean index f649938cab594..371f24725434e 100644 --- a/src/topology/basic.lean +++ b/src/topology/basic.lean @@ -525,7 +525,7 @@ theorem mem_closure_iff_nhds_basis {a : α} {p : β → Prop} {s : β → set α a ∈ closure t ↔ ∀ i, p i → ∃ y ∈ t, y ∈ s i := mem_closure_iff_nhds.trans ⟨λ H i hi, let ⟨x, hx⟩ := (H _ $ h.mem_of_mem hi) in ⟨x, hx.2, hx.1⟩, - λ H t' ht', let ⟨i, hi, hit⟩ := (h t').1 ht', ⟨x, xt, hx⟩ := H i hi in + λ H t' ht', let ⟨i, hi, hit⟩ := h.mem_iff.1 ht', ⟨x, xt, hx⟩ := H i hi in ⟨x, hit hx, xt⟩⟩ /-- `x` belongs to the closure of `s` if and only if some ultrafilter diff --git a/src/topology/continuous_on.lean b/src/topology/continuous_on.lean index 0a3c6b24c34ef..f8d76edec792a 100644 --- a/src/topology/continuous_on.lean +++ b/src/topology/continuous_on.lean @@ -52,11 +52,11 @@ nhds_within_has_basis (nhds_basis_opens a) t theorem mem_nhds_within {t : set α} {a : α} {s : set α} : t ∈ nhds_within a s ↔ ∃ u, is_open u ∧ a ∈ u ∧ u ∩ s ⊆ t := -by simpa only [exists_prop, and_assoc, and_comm] using nhds_within_basis_open a s t +by simpa only [exists_prop, and_assoc, and_comm] using (nhds_within_basis_open a s).mem_iff lemma mem_nhds_within_iff_exists_mem_nhds_inter {t : set α} {a : α} {s : set α} : t ∈ nhds_within a s ↔ ∃ u ∈ 𝓝 a, u ∩ s ⊆ t := -nhds_within_has_basis (𝓝 a).basis_sets s t +(nhds_within_has_basis (𝓝 a).basis_sets s).mem_iff lemma mem_nhds_within_of_mem_nhds {s t : set α} {a : α} (h : s ∈ 𝓝 a) : s ∈ nhds_within a t := diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean index 9b2d9904744c2..5c8d9554f1044 100644 --- a/src/topology/metric_space/basic.lean +++ b/src/topology/metric_space/basic.lean @@ -320,7 +320,7 @@ protected theorem mk_uniformity_basis {β : Type*} {p : β → Prop} {f : β → (hf₀ : ∀ i, p i → 0 < f i) (hf : ∀ ⦃ε⦄, 0 < ε → ∃ i (hi : p i), f i ≤ ε) : (𝓤 α).has_basis p (λ i, {p:α×α | dist p.1 p.2 < f i}) := begin - refine λ s, uniformity_basis_dist.mem_iff.trans _, + refine ⟨λ s, uniformity_basis_dist.mem_iff.trans _⟩, split, { rintros ⟨ε, ε₀, hε⟩, obtain ⟨i, hi, H⟩ : ∃ i (hi : p i), f i ≤ ε, from hf ε₀, @@ -348,7 +348,7 @@ protected theorem mk_uniformity_basis_le {β : Type*} {p : β → Prop} {f : β (hf₀ : ∀ x, p x → 0 < f x) (hf : ∀ ε, 0 < ε → ∃ x (hx : p x), f x ≤ ε) : (𝓤 α).has_basis p (λ x, {p:α×α | dist p.1 p.2 ≤ f x}) := begin - refine λ s, uniformity_basis_dist.mem_iff.trans _, + refine ⟨λ s, uniformity_basis_dist.mem_iff.trans _⟩, split, { rintros ⟨ε, ε₀, hε⟩, rcases dense ε₀ with ⟨ε', hε'⟩, @@ -606,7 +606,7 @@ distance coincide. -/ /-- Expressing the uniformity in terms of `edist` -/ protected lemma metric.uniformity_basis_edist : (𝓤 α).has_basis (λ ε:ennreal, 0 < ε) (λ ε, {p | edist p.1 p.2 < ε}) := -begin +⟨begin intro t, refine mem_uniformity_dist.trans ⟨_, _⟩; rintro ⟨ε, ε0, Hε⟩, { use [ennreal.of_real ε, ennreal.of_real_pos.2 ε0], @@ -617,7 +617,7 @@ begin rw [ennreal.of_real_pos] at ε0', refine ⟨ε', ε0', λ a b h, Hε (lt_trans _ hε)⟩, rwa [edist_dist, ennreal.of_real_lt_of_real_iff ε0'] } -end +end⟩ @[nolint ge_or_gt] -- see Note [nolint_ge] theorem metric.uniformity_edist : 𝓤 α = (⨅ ε>0, principal {p:α×α | edist p.1 p.2 < ε}) := diff --git a/src/topology/metric_space/emetric_space.lean b/src/topology/metric_space/emetric_space.lean index c8e126652ed16..0ede137586a59 100644 --- a/src/topology/metric_space/emetric_space.lean +++ b/src/topology/metric_space/emetric_space.lean @@ -214,7 +214,7 @@ protected theorem emetric.mk_uniformity_basis {β : Type*} {p : β → Prop} {f (hf₀ : ∀ x, p x → 0 < f x) (hf : ∀ ε, 0 < ε → ∃ x (hx : p x), f x ≤ ε) : (𝓤 α).has_basis p (λ x, {p:α×α | edist p.1 p.2 < f x}) := begin - refine λ s, uniformity_basis_edist.mem_iff.trans _, + refine ⟨λ s, uniformity_basis_edist.mem_iff.trans _⟩, split, { rintros ⟨ε, ε₀, hε⟩, rcases hf ε ε₀ with ⟨i, hi, H⟩, @@ -230,7 +230,7 @@ protected theorem emetric.mk_uniformity_basis_le {β : Type*} {p : β → Prop} (hf₀ : ∀ x, p x → 0 < f x) (hf : ∀ ε, 0 < ε → ∃ x (hx : p x), f x ≤ ε) : (𝓤 α).has_basis p (λ x, {p:α×α | edist p.1 p.2 ≤ f x}) := begin - refine λ s, uniformity_basis_edist.mem_iff.trans _, + refine ⟨λ s, uniformity_basis_edist.mem_iff.trans _⟩, split, { rintros ⟨ε, ε₀, hε⟩, rcases dense ε₀ with ⟨ε', hε'⟩, @@ -274,8 +274,8 @@ mem_uniformity_edist.2 ⟨ε, ε0, λ a b, id⟩ namespace emetric -theorem uniformity_has_countable_basis : has_countable_basis (𝓤 α) := -has_countable_basis_of_seq _ _ uniformity_basis_edist_inv_nat.eq_infi +theorem uniformity_has_countable_basis : is_countably_generated (𝓤 α) := +is_countably_generated_of_seq ⟨_, uniformity_basis_edist_inv_nat.eq_infi⟩ /-- ε-δ characterization of uniform continuity on emetric spaces -/ theorem uniform_continuous_iff [emetric_space β] {f : α → β} : @@ -574,7 +574,7 @@ nhds_basis_uniformity uniformity_basis_edist theorem nhds_eq : 𝓝 x = (⨅ε>0, principal (ball x ε)) := nhds_basis_eball.eq_binfi -theorem mem_nhds_iff : s ∈ 𝓝 x ↔ ∃ε>0, ball x ε ⊆ s := nhds_basis_eball s +theorem mem_nhds_iff : s ∈ 𝓝 x ↔ ∃ε>0, ball x ε ⊆ s := nhds_basis_eball.mem_iff theorem is_open_iff : is_open s ↔ ∀x∈s, ∃ε>0, ball x ε ⊆ s := by simp [is_open_iff_nhds, mem_nhds_iff] diff --git a/src/topology/sequences.lean b/src/topology/sequences.lean index 3fcaed05ad9ca..ace615504da43 100644 --- a/src/topology/sequences.lean +++ b/src/topology/sequences.lean @@ -1,11 +1,12 @@ /- Copyright (c) 2018 Jan-David Salchow. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jan-David Salchow +Authors: Jan-David Salchow, Patrick Massot -/ import topology.basic import topology.bases +import topology.subset_properties /-! # Sequences in topological spaces @@ -29,15 +30,16 @@ variables {α : Type*} {β : Type*} local notation f ` ⟶ ` limit := tendsto f at_top (𝓝 limit) -/-! ### Statements about sequences in general topological spaces. -/ +/-! ### Sequential closures, sequential continuity, and sequential spaces. -/ section topological_space variables [topological_space α] [topological_space β] /-- A sequence converges in the sence of topological spaces iff the associated statement for filter holds. -/ +@[nolint ge_or_gt] -- see Note [nolint_ge] lemma topological_space.seq_tendsto_iff {x : ℕ → α} {limit : α} : tendsto x at_top (𝓝 limit) ↔ - ∀ U : set α, limit ∈ U → is_open U → ∃ n0 : ℕ, ∀ n ≥ n0, (x n) ∈ U := + ∀ U : set α, limit ∈ U → is_open U → ∃ N, ∀ n ≥ N, (x n) ∈ U := (at_top_basis.tendsto_iff (nhds_basis_opens limit)).trans $ by simp only [and_imp, exists_prop, true_and, set.mem_Ici, ge_iff_le, id] @@ -142,39 +144,31 @@ namespace topological_space namespace first_countable_topology +variables [topological_space α] [first_countable_topology α] + /-- Every first-countable space is sequential. -/ @[priority 100] -- see Note [lower instance priority] -instance [topological_space α] [first_countable_topology α] : sequential_space α := +instance : sequential_space α := ⟨show ∀ M, sequential_closure M = closure M, from assume M, suffices closure M ⊆ sequential_closure M, from set.subset.antisymm (sequential_closure_subset_closure M) this, -- For every p ∈ closure M, we need to construct a sequence x in M that converges to p: assume (p : α) (hp : p ∈ closure M), - -- Since we are in a first-countable space, there exists a monotonically decreasing - -- sequence g of sets generating the neighborhood filter around p: - exists.elim (mono_seq_of_has_countable_basis _ - (nhds_generated_countable p)) $ assume g ⟨gmon, gbasis⟩, - -- (g i) is a neighborhood of p and hence intersects M. - -- Via choice we obtain the sequence x such that (x i).val ∈ g i ∩ M: - have x : Π i, g i ∩ M, - { rw mem_closure_iff_nhds at hp, - intro i, apply classical.indefinite_description, - apply hp, rw gbasis, rw ← le_principal_iff, apply infi_le_of_le i _, apply le_refl _ }, - -- It remains to show that x converges to p. Intuitively this is the case - -- because x i ∈ g i, and the g i get "arbitrarily small" around p. Formally: - have gssnhds : ∀ s ∈ 𝓝 p, ∃ i, g i ⊆ s, - { intro s, rw gbasis, rw mem_infi, - { simp, intros i hi, use i, assumption }, - { apply directed_of_mono, intros, apply principal_mono.mpr, apply gmon, assumption }, - { apply_instance } }, - -- For the sequence (x i) we can now show that a) it lies in M, and b) converges to p. - ⟨λ i, (x i).val, by intro i; simp [(x i).property.right], - begin - rw tendsto_at_top', intros s nhdss, - rcases gssnhds s nhdss with ⟨i, hi⟩, - use i, intros j hij, apply hi, apply gmon _ _ hij, - simp [(x j).property.left] - end⟩⟩ + -- Since we are in a first-countable space, the neighborhood filter around `p` has a decreasing + -- basis `U` indexed by `ℕ`. + let ⟨U, hU ⟩ := (nhds_generated_countable p).has_antimono_basis in + -- Since `p ∈ closure M`, there is an element in each `M ∩ U i` + have hp : ∀ (i : ℕ), ∃ (y : α), y ∈ M ∧ y ∈ U i, + by simpa using (mem_closure_iff_nhds_basis hU.1).mp hp, + begin + -- The axiom of (countable) choice builds our sequence from the later fact + choose u hu using hp, + rw forall_and_distrib at hu, + -- It clearly takes values in `M` + use [u, hu.1], + -- and converges to `p` because the basis is decreasing. + apply hU.tendsto hu.2, + end⟩ end first_countable_topology diff --git a/src/topology/uniform_space/cauchy.lean b/src/topology/uniform_space/cauchy.lean index 9bb4bc46af601..c8afcb37a398b 100644 --- a/src/topology/uniform_space/cauchy.lean +++ b/src/topology/uniform_space/cauchy.lean @@ -484,7 +484,7 @@ namespace uniform_space open sequentially_complete -variables (H : has_countable_basis (𝓤 α)) +variables (H : is_countably_generated (𝓤 α)) include H @@ -494,7 +494,7 @@ theorem complete_of_convergent_controlled_sequences (U : ℕ → set (α × α)) (HU : ∀ u : ℕ → α, (∀ N m n, N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, tendsto u at_top (𝓝 a)) : complete_space α := begin - rcases (𝓤 α).has_countable_basis_iff_mono_seq'.1 H with ⟨U', U'_mono, hU'⟩, + rcases H.exists_antimono_seq' with ⟨U', U'_mono, hU'⟩, have Hmem : ∀ n, U n ∩ U' n ∈ 𝓤 α, from λ n, inter_mem_sets (U_mem n) (hU'.2 ⟨n, subset.refl _⟩), refine ⟨λ f hf, (HU (seq hf Hmem) (λ N m n hm hn, _)).imp $ @@ -509,7 +509,7 @@ complete. -/ theorem complete_of_cauchy_seq_tendsto (H' : ∀ u : ℕ → α, cauchy_seq u → ∃a, tendsto u at_top (𝓝 a)) : complete_space α := -let ⟨U', U'_mono, hU'⟩ := (𝓤 α).has_countable_basis_iff_mono_seq'.1 H in +let ⟨U', U'_mono, hU'⟩ := H.exists_antimono_seq' in complete_of_convergent_controlled_sequences H U' (λ n, hU'.2 ⟨n, subset.refl _⟩) (λ u hu, H' u $ cauchy_seq_of_controlled U' (λ s hs, hU'.1 hs) hu)