From a423cc75c9bab0b9eb3478b28d8f7625a8d66433 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Tue, 14 Aug 2018 18:43:14 +0200 Subject: [PATCH] refactor(order/filter): simplify filter structure --- analysis/ennreal.lean | 12 +- analysis/real.lean | 2 +- analysis/topology/continuity.lean | 10 +- analysis/topology/topological_space.lean | 4 +- analysis/topology/topological_structures.lean | 20 +- analysis/topology/uniform_space.lean | 62 +++---- data/analysis/filter.lean | 10 +- order/filter.lean | 173 +++++++++--------- order/liminf_limsup.lean | 8 +- 9 files changed, 152 insertions(+), 149 deletions(-) diff --git a/analysis/ennreal.lean b/analysis/ennreal.lean index 109bc84bf45e4..550d8d9d02956 100644 --- a/analysis/ennreal.lean +++ b/analysis/ennreal.lean @@ -71,7 +71,7 @@ by_cases have {x | x < of_real u} ∈ (nhds (of_real r)).sets, by rw [this]; from mem_infi_sets (of_real u) (mem_infi_sets (by simp *) (subset.refl _)), - ((nhds (of_real r)).upwards_sets this $ forall_ennreal.mpr $ + ((nhds (of_real r)).sets_of_superset this $ forall_ennreal.mpr $ by simp [le_of_lt, hu, hl] {contextual := tt}; exact assume p hp _, lt_of_lt_of_le hl hp)) (assume hr_ne : r ≠ 0, have hu0 : 0 < u, from lt_of_le_of_lt hr hu, @@ -111,7 +111,7 @@ le_antisymm (assume : r ≠ 0, have hr' : 0 < r, from lt_of_le_of_ne hr this.symm, have h' : map (of_ennreal ∘ of_real) (nhds r) = map id (nhds r), - from map_cong $ (nhds r).upwards_sets (mem_nhds_sets (is_open_lt' 0) hr') $ + from map_cong $ (nhds r).sets_of_superset (mem_nhds_sets (is_open_lt' 0) hr') $ assume r hr, by simp [le_of_lt hr, (∘)], le_of_map_le_map_inj' h₁ h₂ h $ le_trans (tendsto_of_ennreal hr) $ by simp [h'])) tendsto_of_real @@ -125,7 +125,7 @@ from by_cases (assume s (hs : {a | of_real a ∈ s} ∈ (nhds r ⊓ principal {x | 0 ≤ x}).sets), let ⟨t₁, ht₁, t₂, ht₂, ht⟩ := mem_inf_sets.mp hs in show {a | of_real a ∈ s} ∈ (nhds r).sets, - from (nhds r).upwards_sets ht₁ $ assume a ha, + from (nhds r).sets_of_superset ht₁ $ assume a ha, match le_total 0 a with | or.inl h := have a ∈ t₂, from ht₂ h, ht ⟨ha, this⟩ | or.inr h := @@ -192,7 +192,7 @@ forall_ennreal.mpr $ and.intro (assume _, by_cases (assume : p = 0, tendsto_cong tendsto_const_nhds $ - (nhds ∞).upwards_sets (mem_nhds_sets (is_open_lt' _) (@of_real_lt_infty 1)) $ + (nhds ∞).sets_of_superset (mem_nhds_sets (is_open_lt' _) (@of_real_lt_infty 1)) $ by simp [this]) (assume p0 : p ≠ 0, have p_pos : 0 < p, from lt_of_le_of_ne hp p0.symm, @@ -218,7 +218,7 @@ forall_ennreal.mpr $ and.intro have : 0 < b, from lt_of_le_of_ne ennreal.zero_le hb0.symm, suffices : tendsto ((*) ∞) (nhds b) (nhds ∞), { simpa [hb0] }, apply (tendsto_cong tendsto_const_nhds $ - (nhds b).upwards_sets (mem_nhds_sets (is_open_lt' _) this) _), + (nhds b).sets_of_superset (mem_nhds_sets (is_open_lt' _) this) _), { assume c hc, have : c ≠ 0, from assume h, by simp [h] at hc; contradiction, simp [this] } @@ -313,7 +313,7 @@ by_cases by simpa [le_of_lt h], by rw [nhds_bot_orderable]; from (tendsto_infi.2 $ assume p, tendsto_infi.2 $ assume hp : 0 < p, tendsto_principal.2 $ - (nhds b).upwards_sets (mem_nhds_sets (is_open_lt' (of_real r)) h) $ + (nhds b).sets_of_superset (mem_nhds_sets (is_open_lt' (of_real r)) h) $ by simp [forall_ennreal, hr, le_of_lt, hp] {contextual := tt})) (assume h : ¬ of_real r < b, let ⟨p, hp, hpr, eq⟩ := (le_of_real_iff hr).mp $ not_lt.1 h in diff --git a/analysis/real.lean b/analysis/real.lean index b5a76ffc302a5..f146aa1db1cd0 100644 --- a/analysis/real.lean +++ b/analysis/real.lean @@ -288,7 +288,7 @@ instance : complete_space ℝ := cases exists_forall_ge_and (hg _ $ half_pos ε0) (real.equiv_lim c _ $ half_pos ε0) with n hn, cases hn _ (le_refl _) with h₁ h₂, - refine upwards_sets _ (F n).1.2 (subset.trans _ $ + refine sets_of_superset _ (F n).1.2 (subset.trans _ $ subset.trans (ball_half_subset (G n) h₂) hε), exact λ x h, lt_trans ((F n).2 x (G n) h (G n).2) h₁ end⟩ diff --git a/analysis/topology/continuity.lean b/analysis/topology/continuity.lean index 34a9bb78c3040..36e418e329344 100644 --- a/analysis/topology/continuity.lean +++ b/analysis/topology/continuity.lean @@ -340,7 +340,7 @@ lemma nhds_induced_eq_vmap {a : α} : @nhds α (induced f t) a = vmap f (nhds (f le_antisymm (assume s ⟨s', hs', (h_s : f ⁻¹' s' ⊆ s)⟩, let ⟨t', hsub, ht', hin⟩ := mem_nhds_sets_iff.1 hs' in - (@nhds α (induced f t) a).upwards_sets + (@nhds α (induced f t) a).sets_of_superset begin simp [mem_nhds_sets_iff], exact ⟨preimage f t', preimage_mono hsub, is_open_induced ht', hin⟩ @@ -547,7 +547,7 @@ is_closed_iff_nhds.mpr $ assume ⟨a₁, a₂⟩ h, eq_of_nhds_neq_bot $ assume by rw [←empty_in_sets_eq_bot, mem_inf_sets] at this; exact this in begin rw [nhds_prod_eq, ←empty_in_sets_eq_bot], - apply filter.upwards_sets, + apply filter.sets_of_superset, apply inter_mem_inf_sets (prod_mem_prod ht₁ ht₂) (mem_principal_sets.mpr (subset.refl _)), exact assume ⟨x₁, x₂⟩ ⟨⟨hx₁, hx₂⟩, (heq : x₁ = x₂)⟩, show false, from @h' x₁ ⟨hx₁, heq.symm ▸ hx₂⟩ @@ -779,7 +779,7 @@ begin have ∀i:ι, ∃a, a∈s i ∧ p i ≤ nhds a, from assume i, h i (p i) (ultrafilter_map hf) $ show (λx:Πi:ι, π i, x i) ⁻¹' s i ∈ f.sets, - from f.upwards_sets hfs $ assume x (hx : ∀i, x i ∈ s i), hx i, + from mem_sets_of_superset hfs $ assume x (hx : ∀i, x i ∈ s i), hx i, let ⟨a, ha⟩ := classical.axiom_of_choice this in ⟨a, assume i, (ha i).left, assume i, map_le_iff_le_vmap.mp $ (ha i).right⟩ end @@ -859,7 +859,7 @@ lemma tendsto_extend [regular_space γ] {b : β} {f : α → γ} (de : dense_emb tendsto (de.extend f) (nhds b) (nhds (de.extend f b)) := let φ := {b | tendsto f (vmap e $ nhds b) (nhds $ de.extend f b)} in have hφ : φ ∈ (nhds b).sets, - from (nhds b).upwards_sets hf $ assume b ⟨c, hc⟩, + from (nhds b).sets_of_superset hf $ assume b ⟨c, hc⟩, show tendsto f (vmap e (nhds b)) (nhds (de.extend f b)), from (de.extend_eq hc).symm ▸ hc, assume s hs, let ⟨s'', hs''₁, hs''₂, hs''₃⟩ := nhds_is_closed hs in @@ -883,7 +883,7 @@ have h₂ : t ⊆ de.extend f ⁻¹' closure (f '' (e ⁻¹' t)), from simp, exact de.vmap_nhds_neq_bot end, -(nhds b).upwards_sets +(nhds b).sets_of_superset (show t ∈ (nhds b).sets, from mem_nhds_sets ht₂ ht₃) (calc t ⊆ de.extend f ⁻¹' closure (f '' (e ⁻¹' t)) : h₂ ... ⊆ de.extend f ⁻¹' closure (f '' (e ⁻¹' s')) : diff --git a/analysis/topology/topological_space.lean b/analysis/topology/topological_space.lean index 967dc45dcc2fc..e449aba48653f 100644 --- a/analysis/topology/topological_space.lean +++ b/analysis/topology/topological_space.lean @@ -544,7 +544,7 @@ assume f hfn hfs, classical.by_contradiction $ assume : ¬ (∃x∈s, f ⊓ nhds have ∅ ∈ (nhds x ⊓ f).sets, by rw [empty_in_sets_eq_bot, hf x hxs], let ⟨t₁, ht₁, t₂, ht₂, ht⟩ := by rw [mem_inf_sets] at this; exact this in have ∅ ∈ (nhds x ⊓ principal t₂).sets, - from (nhds x ⊓ principal t₂).upwards_sets (inter_mem_inf_sets ht₁ (subset.refl t₂)) ht, + from (nhds x ⊓ principal t₂).sets_of_superset (inter_mem_inf_sets ht₁ (subset.refl t₂)) ht, have nhds x ⊓ principal t₂ = ⊥, by rwa [empty_in_sets_eq_bot] at this, by simp [closure_eq_nhds] at hx; exact hx t₂ ht₂ this, @@ -559,7 +559,7 @@ assume f hfn hfs, classical.by_contradiction $ assume : ¬ (∃x∈s, f ⊓ nhds have s ∩ (⋂s∈c', if h : s ∈ c' then b ⟨s, h⟩ else univ) ∈ f.sets, from inter_mem_sets (by simp at hfs; assumption) this, have ∅ ∈ f.sets, - from f.upwards_sets this $ assume x ⟨hxs, hxi⟩, + from mem_sets_of_superset this $ assume x ⟨hxs, hxi⟩, let ⟨t, htc', hxt⟩ := (show ∃t ∈ c', x ∈ t, by simpa using hsc' hxs) in have -closure (b ⟨t, htc'⟩) = t, from (hb _).right, have x ∈ - t, diff --git a/analysis/topology/topological_structures.lean b/analysis/topology/topological_structures.lean index 5bc84bafb054c..004f92c2b9d8d 100644 --- a/analysis/topology/topological_structures.lean +++ b/analysis/topology/topological_structures.lean @@ -408,13 +408,13 @@ lemma lt_mem_nhds {a b : α} (h : a < b) : {b | a < b} ∈ (nhds b).sets := mem_nhds_sets (is_open_lt' _) h lemma le_mem_nhds {a b : α} (h : a < b) : {b | a ≤ b} ∈ (nhds b).sets := -(nhds b).upwards_sets (lt_mem_nhds h) $ assume b hb, le_of_lt hb +(nhds b).sets_of_superset (lt_mem_nhds h) $ assume b hb, le_of_lt hb lemma gt_mem_nhds {a b : α} (h : a < b) : {a | a < b} ∈ (nhds a).sets := mem_nhds_sets (is_open_gt' _) h lemma ge_mem_nhds {a b : α} (h : a < b) : {a | a ≤ b} ∈ (nhds a).sets := -(nhds a).upwards_sets (gt_mem_nhds h) $ assume b hb, le_of_lt hb +(nhds a).sets_of_superset (gt_mem_nhds h) $ assume b hb, le_of_lt hb lemma nhds_eq_orderable {a : α} : nhds a = (⨅ba, principal {c | c < b}) := @@ -622,10 +622,10 @@ instance orderable_topology.regular_space : regular_space α := | or.inl ⟨b, hb₁, hb₂⟩ := ⟨{a | a < b}, is_open_gt' _, assume c hcs hca, show c < b, from lt_of_not_ge $ assume hbc, h c (lt_of_lt_of_le hb₁ hbc) (le_of_lt hca) hcs, - inf_principal_eq_bot $ (nhds a).upwards_sets (mem_nhds_sets (is_open_lt' _) hb₂) $ + inf_principal_eq_bot $ (nhds a).sets_of_superset (mem_nhds_sets (is_open_lt' _) hb₂) $ assume x (hx : b < x), show ¬ x < b, from not_lt.2 $ le_of_lt hx⟩ | or.inr ⟨h₁, h₂⟩ := ⟨{a' | a' < a}, is_open_gt' _, assume b hbs hba, hba, - inf_principal_eq_bot $ (nhds a).upwards_sets (mem_nhds_sets (is_open_lt' _) hl) $ + inf_principal_eq_bot $ (nhds a).sets_of_superset (mem_nhds_sets (is_open_lt' _) hl) $ assume x (hx : l < x), show ¬ x < a, from not_lt.2 $ h₁ _ hx⟩ end) (assume : ¬ ∃l, l < a, ⟨∅, is_open_empty, assume l _ hl, (this ⟨l, hl⟩).elim, @@ -639,10 +639,10 @@ instance orderable_topology.regular_space : regular_space α := | or.inl ⟨b, hb₁, hb₂⟩ := ⟨{a | b < a}, is_open_lt' _, assume c hcs hca, show c > b, from lt_of_not_ge $ assume hbc, h c (le_of_lt hca) (lt_of_le_of_lt hbc hb₂) hcs, - inf_principal_eq_bot $ (nhds a).upwards_sets (mem_nhds_sets (is_open_gt' _) hb₁) $ + inf_principal_eq_bot $ (nhds a).sets_of_superset (mem_nhds_sets (is_open_gt' _) hb₁) $ assume x (hx : b > x), show ¬ x > b, from not_lt.2 $ le_of_lt hx⟩ | or.inr ⟨h₁, h₂⟩ := ⟨{a' | a' > a}, is_open_lt' _, assume b hbs hba, hba, - inf_principal_eq_bot $ (nhds a).upwards_sets (mem_nhds_sets (is_open_gt' _) hu) $ + inf_principal_eq_bot $ (nhds a).sets_of_superset (mem_nhds_sets (is_open_gt' _) hu) $ assume x (hx : u > x), show ¬ x > a, from not_lt.2 $ h₂ _ hx⟩ end) (assume : ¬ ∃u, u > a, ⟨∅, is_open_empty, assume l _ hl, (this ⟨l, hl⟩).elim, @@ -889,13 +889,13 @@ theorem lt_mem_sets_of_Limsup_lt {f : filter α} {b} (h : f.is_bounded (≤)) (l {a | a < b} ∈ f.sets := let ⟨c, (h : {a : α | a ≤ c} ∈ f.sets), hcb⟩ := exists_lt_of_cInf_lt (ne_empty_iff_exists_mem.2 h) l in -f.upwards_sets h $ assume a hac, lt_of_le_of_lt hac hcb +mem_sets_of_superset h $ assume a hac, lt_of_le_of_lt hac hcb theorem gt_mem_sets_of_Liminf_gt {f : filter α} {b} (h : f.is_bounded (≥)) (l : f.Liminf > b) : {a | a > b} ∈ f.sets := let ⟨c, (h : {a : α | c ≤ a} ∈ f.sets), hbc⟩ := exists_lt_of_lt_cSup (ne_empty_iff_exists_mem.2 h) l in -f.upwards_sets h $ assume a hca, lt_of_lt_of_le hbc hca +mem_sets_of_superset h $ assume a hca, lt_of_lt_of_le hbc hca /-- If the liminf and the limsup of a filter coincide, then this filter converges to their common value, at least if the filter is eventually bounded above and below. -/ @@ -912,7 +912,7 @@ cInf_intro (ne_empty_iff_exists_mem.2 $ is_bounded_le_nhds a) (assume b (hba : a < b), show ∃c (h : {n : α | n ≤ c} ∈ (nhds a).sets), c < b, from match dense_or_discrete hba with | or.inl ⟨c, hac, hcb⟩ := ⟨c, ge_mem_nhds hac, hcb⟩ - | or.inr ⟨_, h⟩ := ⟨a, (nhds a).upwards_sets (gt_mem_nhds hba) h, hba⟩ + | or.inr ⟨_, h⟩ := ⟨a, (nhds a).sets_of_superset (gt_mem_nhds hba) h, hba⟩ end) theorem Liminf_nhds (a : α) : Liminf (nhds a) = a := @@ -921,7 +921,7 @@ cSup_intro (ne_empty_iff_exists_mem.2 $ is_bounded_ge_nhds a) (assume b (hba : b < a), show ∃c (h : {n : α | c ≤ n} ∈ (nhds a).sets), b < c, from match dense_or_discrete hba with | or.inl ⟨c, hbc, hca⟩ := ⟨c, le_mem_nhds hca, hbc⟩ - | or.inr ⟨h, _⟩ := ⟨a, (nhds a).upwards_sets (lt_mem_nhds hba) h, hba⟩ + | or.inr ⟨h, _⟩ := ⟨a, (nhds a).sets_of_superset (lt_mem_nhds hba) h, hba⟩ end) /-- If a filter is converging, its limsup coincides with its limit. -/ diff --git a/analysis/topology/uniform_space.lean b/analysis/topology/uniform_space.lean index 81eb2a4930092..f0a9ce580d78d 100644 --- a/analysis/topology/uniform_space.lean +++ b/analysis/topology/uniform_space.lean @@ -259,22 +259,22 @@ lemma mem_nhds_uniformity_iff {x : α} {s : set α} : hs⟩⟩ lemma nhds_eq_vmap_uniformity {x : α} : nhds x = uniformity.vmap (prod.mk x) := -filter.ext.2 $ assume s, by rw [mem_nhds_uniformity_iff, mem_vmap_sets]; from iff.intro +by ext s; rw [mem_nhds_uniformity_iff, mem_vmap_sets]; from iff.intro (assume hs, ⟨_, hs, assume x hx, hx rfl⟩) - (assume ⟨t, h, ht⟩, uniformity.upwards_sets h $ + (assume ⟨t, h, ht⟩, uniformity.sets_of_superset h $ assume ⟨p₁, p₂⟩ hp (h : p₁ = x), ht $ by simp [h.symm, hp]) lemma nhds_eq_uniformity {x : α} : nhds x = uniformity.lift' (λs:set (α×α), {y | (x, y) ∈ s}) := -filter_eq $ set.ext $ assume s, - begin - rw [mem_lift'_sets], tactic.swap, apply monotone_preimage, - simp [mem_nhds_uniformity_iff], - exact ⟨assume h, ⟨_, h, assume y h, h rfl⟩, - assume ⟨t, h₁, h₂⟩, - uniformity.upwards_sets h₁ $ - assume ⟨x', y⟩ hp (eq : x' = x), h₂ $ - show (x, y) ∈ t, from eq ▸ hp⟩ - end +begin + ext s, + rw [mem_lift'_sets], tactic.swap, apply monotone_preimage, + simp [mem_nhds_uniformity_iff], + exact ⟨assume h, ⟨_, h, assume y h, h rfl⟩, + assume ⟨t, h₁, h₂⟩, + uniformity.sets_of_superset h₁ $ + assume ⟨x', y⟩ hp (eq : x' = x), h₂ $ + show (x, y) ∈ t, from eq ▸ hp⟩ +end lemma mem_nhds_left (x : α) {s : set (α×α)} (h : s ∈ (uniformity.sets : set (set (α×α)))) : {y : α | (x, y) ∈ s} ∈ (nhds x).sets := @@ -404,7 +404,7 @@ le_antisymm assume x, assume : x ∈ t, let ⟨x, y, h₁, h₂, h₃⟩ := ht_comp this in hs_comp ⟨x, h₁, y, h₂, h₃⟩, have interior d ∈ (@uniformity α _).sets, by filter_upwards [hs] this, by simp [this]) - (assume s hs, (uniformity.lift' interior).upwards_sets (mem_lift' hs) interior_subset) + (assume s hs, (uniformity.lift' interior).sets_of_superset (mem_lift' hs) interior_subset) lemma interior_mem_uniformity {s : set (α × α)} (hs : s ∈ (@uniformity α _).sets) : interior s ∈ (@uniformity α _).sets := @@ -416,7 +416,7 @@ have s ∈ ((@uniformity α _).lift' closure).sets, by rwa [uniformity_eq_unifor have ∃t∈(@uniformity α _).sets, closure t ⊆ s, by rwa [mem_lift'_sets] at this; apply closure_mono, let ⟨t, ht, hst⟩ := this in -⟨closure t, uniformity.upwards_sets ht subset_closure, is_closed_closure, hst⟩ +⟨closure t, uniformity.sets_of_superset ht subset_closure, is_closed_closure, hst⟩ /- uniform continuity -/ @@ -445,7 +445,7 @@ vmap (λx:α×α, (f x.1, f x.2)) uniformity = uniformity theorem uniform_embedding_def [uniform_space β] {f : α → β} : uniform_embedding f ↔ function.injective f ∧ ∀ s, s ∈ (@uniformity α _).sets ↔ ∃ t ∈ (@uniformity β _).sets, ∀ x y : α, (f x, f y) ∈ t → (x, y) ∈ s := -by rw [uniform_embedding, eq_comm, filter.ext]; simp [subset_def] +by rw [uniform_embedding, eq_comm, filter.ext_iff]; simp [subset_def] theorem uniform_embedding_def' [uniform_space β] {f : α → β} : uniform_embedding f ↔ function.injective f ∧ uniform_continuous f ∧ @@ -454,7 +454,7 @@ theorem uniform_embedding_def' [uniform_space β] {f : α → β} : by simp [uniform_embedding_def, uniform_continuous_def]; exact ⟨λ ⟨I, H⟩, ⟨I, λ s su, (H _).2 ⟨s, su, λ x y, id⟩, λ s, (H s).1⟩, λ ⟨I, H₁, H₂⟩, ⟨I, λ s, ⟨H₂ s, - λ ⟨t, tu, h⟩, upwards_sets _ (H₁ t tu) (λ ⟨a, b⟩, h a b)⟩⟩⟩ + λ ⟨t, tu, h⟩, sets_of_superset _ (H₁ t tu) (λ ⟨a, b⟩, h a b)⟩⟩⟩ lemma uniform_embedding.uniform_continuous [uniform_space β] {f : α → β} (hf : uniform_embedding f) : uniform_continuous f := @@ -526,7 +526,7 @@ begin end, have ∀b', (b, b') ∈ t → b' ∈ closure (e '' {a' | (a, a') ∈ s}), from assume b' hb', by rw [closure_eq_nhds]; exact this b' hb', -⟨a, (nhds b).upwards_sets (mem_nhds_left b htu) this⟩ +⟨a, (nhds b).sets_of_superset (mem_nhds_left b htu) this⟩ /-- A filter `f` is Cauchy if for every entourage `r`, there exists an `s ∈ f` such that `s × s ⊆ r`. This is a generalization of Cauchy @@ -571,7 +571,7 @@ calc f ≤ f.lift' (λs:set α, {y | x ∈ closure s ∧ y ∈ closure s}) : begin rw [←forall_sets_neq_empty_iff_neq_bot] at adhs, simp [this s hs], - exact f.upwards_sets hs subset_closure + exact mem_sets_of_superset hs subset_closure end ... ≤ f.lift' (λs:set α, {y | (x, y) ∈ closure (set.prod s s)}) : by simp [closure_prod_eq]; exact le_refl _ @@ -689,7 +689,7 @@ instance separated_regular [separated α] : regular_space α := let ⟨x, (hx : (a, x) ∈ d), y, ⟨hx₁, hx₂⟩, (hy : (y, _) ∈ d)⟩ := @this ⟨a, a'⟩ ⟨hae, ha'⟩ in have (a, a') ∈ comp_rel d d, from ⟨y, hx₂, hy⟩, h this rfl, - have closure e ∈ (nhds a).sets, from (nhds a).upwards_sets (mem_nhds_left a hd) subset_closure, + have closure e ∈ (nhds a).sets, from (nhds a).sets_of_superset (mem_nhds_left a hd) subset_closure, have nhds a ⊓ principal (-closure e) = ⊥, from (@inf_eq_bot_iff_le_compl _ _ _ (principal (- closure e)) (principal (closure e)) (by simp [principal_univ, union_comm]) (by simp)).mpr (by simp [this]), @@ -770,14 +770,14 @@ lemma cauchy_of_totally_bounded_of_ultrafilter {s : set α} {f : filter α} let ⟨t', ht'₁, ht'_symm, ht'_t⟩ := comp_symm_of_uniformity ht in let ⟨i, hi, hs_union⟩ := hs t' ht'₁ in have (⋃y∈i, {x | (x,y) ∈ t'}) ∈ f.sets, - from f.upwards_sets (le_principal_iff.mp h) hs_union, + from mem_sets_of_superset (le_principal_iff.mp h) hs_union, have ∃y∈i, {x | (x,y) ∈ t'} ∈ f.sets, from mem_of_finite_Union_ultrafilter hf hi this, let ⟨y, hy, hif⟩ := this in have set.prod {x | (x,y) ∈ t'} {x | (x,y) ∈ t'} ⊆ comp_rel t' t', from assume ⟨x₁, x₂⟩ ⟨(h₁ : (x₁, y) ∈ t'), (h₂ : (x₂, y) ∈ t')⟩, ⟨y, h₁, ht'_symm h₂⟩, - (filter.prod f f).upwards_sets (prod_mem_prod hif hif) (subset.trans this ht'_t)⟩ + (filter.prod f f).sets_of_superset (prod_mem_prod hif hif) (subset.trans this ht'_t)⟩ lemma totally_bounded_iff_filter {s : set α} : totally_bounded s ↔ (∀f, f ≠ ⊥ → f ≤ principal s → ∃c ≤ f, cauchy c) := @@ -821,7 +821,7 @@ lemma totally_bounded_iff_filter {s : set α} : have (s - ys) ∩ (m ∩ s) ∈ c.sets, from inter_mem_sets (le_principal_iff.mp this) ‹m ∩ s ∈ c.sets›, have ∅ ∈ c.sets, - from c.upwards_sets this $ assume x ⟨⟨hxs, hxys⟩, hxm, _⟩, hxys $ ‹m ⊆ ys› hxm, + from c.sets_of_superset this $ assume x ⟨⟨hxs, hxys⟩, hxm, _⟩, hxys $ ‹m ⊆ ys› hxm, hc₂.left $ empty_in_sets_eq_bot.mp this⟩ lemma totally_bounded_iff_ultrafilter {s : set α} : @@ -879,7 +879,7 @@ have mp₁ : ∀{s}, monotone (p s), have f ≤ g, from le_infi $ assume s, le_infi $ assume hs, le_infi $ assume t, le_infi $ assume ht, le_principal_iff.mpr $ - f.upwards_sets ht $ assume x hx, ⟨x, hx, refl_mem_uniformity hs⟩, + mem_sets_of_superset ht $ assume x hx, ⟨x, hx, refl_mem_uniformity hs⟩, have g ≠ ⊥, from neq_bot_of_le_neq_bot hf.left this, @@ -911,7 +911,7 @@ have cauchy g, from from mem_lift hs₂ $ @mem_lift' α α f _ t ht, have hg : set.prod (p (preimage prod.swap s₁) t) (p s₂ t) ∈ (filter.prod g g).sets, from @prod_mem_prod α α _ _ g g hg₁ hg₂, - (filter.prod g g).upwards_sets hg + (filter.prod g g).sets_of_superset hg (assume ⟨a, b⟩ ⟨⟨c₁, c₁t, hc₁⟩, ⟨c₂, c₂t, hc₂⟩⟩, have (c₁, c₂) ∈ set.prod t t, from ⟨c₁t, c₂t⟩, comp_s₁ $ prod_mk_mem_comp_rel hc₁ $ @@ -972,8 +972,8 @@ instance {α : Type u} [u : uniform_space α] : uniform_space (quotient (separat from assume a₁ a₂ ha₁ ha₂, @hts (a, a₂) ⟨a₁, ha₁, ha₂⟩ rfl, have ht' : ∀{a₁ a₂}, a₁ ≈ a₂ → (a₁, a₂) ∈ t, from assume a₁ a₂ h, sInter_subset_of_mem ht h, - uniformity.upwards_sets ht $ assume ⟨a₁, a₂⟩ h₁ h₂, hts (ht' $ setoid.symm h₂) h₁, - assume h, uniformity.upwards_sets h $ by simp {contextual := tt}⟩, + uniformity.sets_of_superset ht $ assume ⟨a₁, a₂⟩ h₁ h₂, hts (ht' $ setoid.symm h₂) h₁, + assume h, uniformity.sets_of_superset h $ by simp {contextual := tt}⟩, begin simp [topological_space.coinduced, u.is_open_uniformity, uniformity, forall_quotient_iff], exact ⟨λh a ha, (this a ha).mp $ h a ha, λh a ha, (this a ha).mpr $ h a ha⟩ @@ -988,7 +988,7 @@ assume t' ht', let ⟨t, ht, tt_t'⟩ := comp_mem_uniformity_sets ht' in let ⟨s, hs, ss_t⟩ := comp_mem_uniformity_sets ht in ⟨(λp:α×α, (⟦p.1⟧, ⟦p.2⟧)) '' s, - (@uniformity α _).upwards_sets hs $ assume x hx, ⟨x, hx, rfl⟩, + (@uniformity α _).sets_of_superset hs $ assume x hx, ⟨x, hx, rfl⟩, assume ⟨a₁, a₂⟩ ⟨⟨b₁, b₂⟩, hb, ab_eq⟩, have ⟦b₁⟧ = ⟦a₁⟧ ∧ ⟦b₂⟧ = ⟦a₂⟧, from prod.mk.inj ab_eq, have b₁ ≈ a₁ ∧ b₂ ≈ a₂, from and.imp quotient.exact quotient.exact this, @@ -1076,7 +1076,7 @@ have preimage (λp:β×β, (f p.1, f p.2)) s ∈ (vmap (λx:β×β, (e x.1, e x. by rwa [h_e.right.symm] at this, let ⟨t, ht, ts⟩ := this in show preimage (λp:(α×α), (ψ p.1, ψ p.2)) d ∈ uniformity.sets, - from (@uniformity α _).upwards_sets (interior_mem_uniformity ht) $ + from (@uniformity α _).sets_of_superset (interior_mem_uniformity ht) $ assume ⟨x₁, x₂⟩ hx_t, have nhds (x₁, x₂) ≤ principal (interior t), from is_open_iff_nhds.mp is_open_interior (x₁, x₂) hx_t, @@ -1150,7 +1150,7 @@ have t₂ ∩ t₃ ∈ h.val.sets, from inter_mem_sets ht₂ ht₃, let ⟨x, xt₂, xt₃⟩ := inhabited_of_mem_sets (h.property.left) this in -(filter.prod f.val g.val).upwards_sets +(filter.prod f.val g.val).sets_of_superset (prod_mem_prod ht₁ ht₄) (assume ⟨a, b⟩ ⟨(ha : a ∈ t₁), (hb : b ∈ t₄)⟩, ⟨x, @@ -1249,8 +1249,8 @@ complete_space_extension let ⟨t, ht₁, (ht₂ : gen t ⊆ s)⟩ := (mem_lift'_sets monotone_gen).mp hs in let ⟨t', ht', (h : set.prod t' t' ⊆ t)⟩ := mem_prod_same_iff.mp (hf.right ht₁) in have t' ⊆ { y : α | (f', pure_cauchy y) ∈ gen t }, - from assume x hx, (filter.prod f (pure x)).upwards_sets (prod_mem_prod ht' $ mem_pure hx) h, - f.upwards_sets ht' $ subset.trans this (preimage_mono ht₂), + from assume x hx, (filter.prod f (pure x)).sets_of_superset (prod_mem_prod ht' $ mem_pure hx) h, + f.sets_of_superset ht' $ subset.trans this (preimage_mono ht₂), ⟨f', by simp [nhds_eq_uniformity]; assumption⟩ end diff --git a/data/analysis/filter.lean b/data/analysis/filter.lean index 24cd91f6c78b1..5e25a630030d4 100644 --- a/data/analysis/filter.lean +++ b/data/analysis/filter.lean @@ -45,11 +45,11 @@ end /-- The filter represented by a `cfilter` is the collection of supersets of elements of the filter base. -/ def to_filter (F : cfilter (set α) σ) : filter α := -{ sets := {a | ∃ b, F b ⊆ a}, - exists_mem_sets := ⟨_, F.pt, subset.refl _⟩, - upwards_sets := λ x y ⟨b, h⟩ s, ⟨b, subset.trans h s⟩, - directed_sets := λ x ⟨a, h₁⟩ y ⟨b, h₂⟩, ⟨_, ⟨F.inf a b, subset.refl _⟩, - subset.trans (F.inf_le_left _ _) h₁, subset.trans (F.inf_le_right _ _) h₂⟩ } +{ sets := {a | ∃ b, F b ⊆ a}, + univ_sets := ⟨F.pt, subset_univ _⟩, + sets_of_superset := λ x y ⟨b, h⟩ s, ⟨b, subset.trans h s⟩, + inter_sets := λ x y ⟨a, h₁⟩ ⟨b, h₂⟩, ⟨F.inf a b, + subset_inter (subset.trans (F.inf_le_left _ _) h₁) (subset.trans (F.inf_le_right _ _) h₂)⟩ } @[simp] theorem mem_to_filter_sets (F : cfilter (set α) σ) {a : set α} : a ∈ F.to_filter.sets ↔ ∃ b, F b ⊆ a := iff.rfl diff --git a/order/filter.lean b/order/filter.lean index 82e91e740e424..e74db76a2705c 100644 --- a/order/filter.lean +++ b/order/filter.lean @@ -5,7 +5,7 @@ Authors: Johannes Hölzl Theory of filters on sets. -/ -import order.complete_lattice order.galois_connection data.set data.finset order.zorn +import order.galois_connection data.set data.finset order.zorn open lattice set universes u v w x y @@ -34,6 +34,7 @@ by simp end +-- TODO: move lemma inf_left_comm [semilattice_inf α] (a b c : α) : a ⊓ (b ⊓ c) = b ⊓ (a ⊓ c) := by rw [← inf_assoc, ← inf_assoc, @inf_comm α _ a] @@ -85,11 +86,11 @@ assume ⟨a, ha⟩ ⟨b, hb⟩, classical.by_cases (assume : f b ≤ f a, ⟨⟨b, hb⟩, this, le_refl _⟩) (assume : f a ≤ f b, ⟨⟨a, ha⟩, le_refl _, this⟩)) -structure filter (α : Type u) := -(sets : set (set α)) -(exists_mem_sets : ∃x, x ∈ sets) -(upwards_sets : ∀{x y}, x ∈ sets → x ⊆ y → y ∈ sets) -(directed_sets : directed_on (⊆) sets) +structure filter (α : Type*) := +(sets : set (set α)) +(univ_sets : set.univ ∈ sets) +(sets_of_superset {x y} : x ∈ sets → x ⊆ y → y ∈ sets) +(inter_sets {x y} : x ∈ sets → y ∈ sets → x ∩ y ∈ sets) namespace filter variables {α : Type u} {f g : filter α} {s t : set α} @@ -100,21 +101,27 @@ lemma filter_eq : ∀{f g : filter α}, f.sets = g.sets → f = g lemma filter_eq_iff : f = g ↔ f.sets = g.sets := ⟨congr_arg _, filter_eq⟩ -lemma filter.ext : f = g ↔ ∀ s, s ∈ f.sets ↔ s ∈ g.sets := +protected lemma ext_iff : f = g ↔ ∀ s, s ∈ f.sets ↔ s ∈ g.sets := by rw [filter_eq_iff, ext_iff] -lemma univ_mem_sets' (h : ∀ a, a ∈ s): s ∈ f.sets := -let ⟨x, x_in_s⟩ := f.exists_mem_sets in f.upwards_sets x_in_s (assume x _, h x) +@[extensionality] +protected lemma ext : (∀ s, s ∈ f.sets ↔ s ∈ g.sets) → f = g := +filter.ext_iff.2 lemma univ_mem_sets : univ ∈ f.sets := -univ_mem_sets' mem_univ +f.univ_sets + +lemma mem_sets_of_superset : ∀{x y : set α}, x ∈ f.sets → x ⊆ y → y ∈ f.sets := +f.sets_of_superset -lemma inter_mem_sets (hs : s ∈ f.sets) (ht : t ∈ f.sets) : s ∩ t ∈ f.sets := -let ⟨z, ⟨z_in_s, z_le_x, z_le_y⟩⟩ := f.directed_sets _ hs _ ht in -f.upwards_sets z_in_s (subset_inter z_le_x z_le_y) +lemma inter_mem_sets : ∀{s t}, s ∈ f.sets → t ∈ f.sets → s ∩ t ∈ f.sets := +f.inter_sets + +lemma univ_mem_sets' (h : ∀ a, a ∈ s): s ∈ f.sets := +mem_sets_of_superset univ_mem_sets (assume x _, h x) lemma mp_sets (hs : s ∈ f.sets) (h : {x | x ∈ s → x ∈ t} ∈ f.sets) : t ∈ f.sets := -f.upwards_sets (inter_mem_sets hs h) $ assume x ⟨h₁, h₂⟩, h₂ h₁ +mem_sets_of_superset (inter_mem_sets hs h) $ assume x ⟨h₁, h₂⟩, h₂ h₁ lemma Inter_mem_sets {β : Type v} {s : β → set α} {is : set β} (hf : finite is) : (∀i∈is, s i ∈ f.sets) → (⋂i∈is, s i) ∈ f.sets := @@ -126,10 +133,10 @@ finite.induction_on hf by simp [inter_mem_sets h₁ h₂]) lemma exists_sets_subset_iff : (∃t∈f.sets, t ⊆ s) ↔ s ∈ f.sets := -⟨assume ⟨t, ht, ts⟩, f.upwards_sets ht ts, assume hs, ⟨s, hs, subset.refl _⟩⟩ +⟨assume ⟨t, ht, ts⟩, mem_sets_of_superset ht ts, assume hs, ⟨s, hs, subset.refl _⟩⟩ lemma monotone_mem_sets {f : filter α} : monotone (λs, s ∈ f.sets) := -assume s t hst h, f.upwards_sets h hst +assume s t hst h, mem_sets_of_superset h hst end filter @@ -161,10 +168,10 @@ section principal /-- The principal filter of `s` is the collection of all supersets of `s`. -/ def principal (s : set α) : filter α := -{ sets := {t | s ⊆ t}, - exists_mem_sets := ⟨s, subset.refl _⟩, - upwards_sets := assume x y hx hy, subset.trans hx hy, - directed_sets := assume x hx y hy, ⟨s, subset.refl _, hx, hy⟩ } +{ sets := {t | s ⊆ t}, + univ_sets := subset_univ s, + sets_of_superset := assume x y hx hy, subset.trans hx hy, + inter_sets := assume x y, subset_inter } instance : inhabited (filter α) := ⟨principal ∅⟩ @@ -177,15 +184,14 @@ end principal section join -/-- The join of a filter of filters is defined by the relation - `s ∈ join f ↔ {t | s ∈ t} ∈ f`. -/ +/-- The join of a filter of filters is defined by the relation `s ∈ join f ↔ {t | s ∈ t} ∈ f`. -/ def join (f : filter (filter α)) : filter α := -{ sets := {s | {t : filter α | s ∈ t.sets} ∈ f.sets}, - exists_mem_sets := ⟨univ, by simp [univ_mem_sets]; exact univ_mem_sets⟩, - upwards_sets := assume x y hx xy, f.upwards_sets hx $ assume a h, a.upwards_sets h xy, - directed_sets := assume x hx y hy, ⟨x ∩ y, - by filter_upwards [hx, hy] assume z h₁ h₂, inter_mem_sets h₁ h₂, - inter_subset_left _ _, inter_subset_right _ _⟩ } +{ sets := {s | {t : filter α | s ∈ t.sets} ∈ f.sets}, + univ_sets := by simp [univ_mem_sets]; exact univ_mem_sets, + sets_of_superset := assume x y hx xy, + mem_sets_of_superset hx $ assume f h, mem_sets_of_superset h xy, + inter_sets := assume x y hx hy, + mem_sets_of_superset (inter_mem_sets hx hy) $ assume f ⟨h₁, h₂⟩, inter_mem_sets h₁ h₂ } @[simp] lemma mem_join_sets {s : set α} {f : filter (filter α)} : s ∈ (join f).sets ↔ {t | s ∈ filter.sets t} ∈ f.sets := iff.rfl @@ -204,7 +210,7 @@ theorem le_def {f g : filter α} : f ≤ g ↔ ∀ x ∈ g.sets, x ∈ f.sets := @[simp] lemma le_principal_iff {s : set α} {f : filter α} : f ≤ principal s ↔ s ∈ f.sets := show (∀{t}, s ⊆ t → t ∈ f.sets) ↔ s ∈ f.sets, - from ⟨assume h, h (subset.refl s), assume hs t ht, f.upwards_sets hs ht⟩ + from ⟨assume h, h (subset.refl s), assume hs t ht, mem_sets_of_superset hs ht⟩ lemma principal_mono {s t : set α} : principal s ≤ principal t ↔ s ⊆ t := by simp @@ -219,12 +225,11 @@ by simp [le_antisymm_iff]; refl of filters is reverse subset. -/ instance : has_sup (filter α) := ⟨λf g : filter α, { sets := f.sets ∩ g.sets, - exists_mem_sets := ⟨univ, by simp [univ_mem_sets]; exact univ_mem_sets⟩, - upwards_sets := assume x y hx xy, - and.imp (assume h, f.upwards_sets h xy) (assume h, g.upwards_sets h xy) hx, - directed_sets := assume x ⟨hx₁, hx₂⟩ y ⟨hy₁, hy₂⟩, ⟨x ∩ y, - ⟨inter_mem_sets hx₁ hy₁, inter_mem_sets hx₂ hy₂⟩, - inter_subset_left _ _, inter_subset_right _ _⟩ }⟩ + univ_sets := ⟨univ_mem_sets, univ_mem_sets⟩, + sets_of_superset := assume x y hx xy, + and.imp (assume h, mem_sets_of_superset h xy) (assume h, mem_sets_of_superset h xy) hx, + inter_sets := assume x y ⟨hx₁, hx₂⟩ ⟨hy₁, hy₂⟩, + ⟨inter_mem_sets hx₁ hy₁, inter_mem_sets hx₂ hy₂⟩ }⟩ @[simp] lemma mem_sup_sets {f g : filter α} {s : set α} : s ∈ (f ⊔ g).sets ↔ s ∈ f.sets ∧ s ∈ g.sets := iff.rfl @@ -232,16 +237,13 @@ instance : has_sup (filter α) := ⟨λf g : filter α, /-- The infimum of filters is the filter generated by intersections of elements of the two filters. -/ instance : has_inf (filter α) := ⟨λf g : filter α, -{ sets := {s | ∃ (a ∈ f.sets) (b ∈ g.sets), a ∩ b ⊆ s }, - exists_mem_sets := ⟨univ, univ, univ_mem_sets, univ, univ_mem_sets, subset_univ _⟩, - upwards_sets := assume x y ⟨a, ha, b, hb, h⟩ xy, - ⟨a, ha, b, hb, subset.trans h xy⟩, - directed_sets := assume x ⟨a₁, ha₁, b₁, hb₁, h₁⟩ y ⟨a₂, ha₂, b₂, hb₂, h₂⟩, - ⟨x ∩ y, - ⟨_, inter_mem_sets ha₁ ha₂, _, inter_mem_sets hb₁ hb₂, - calc (a₁ ⊓ a₂) ⊓ (b₁ ⊓ b₂) = (a₁ ⊓ b₁) ⊓ (a₂ ⊓ b₂) : by ac_refl - ... ≤ x ∩ y : inf_le_inf h₁ h₂ ⟩, - inter_subset_left _ _, inter_subset_right _ _⟩ }⟩ +{ sets := {s | ∃ (a ∈ f.sets) (b ∈ g.sets), a ∩ b ⊆ s }, + univ_sets := ⟨_, univ_mem_sets, _, univ_mem_sets, inter_subset_left _ _⟩, + sets_of_superset := assume x y ⟨a, ha, b, hb, h⟩ xy, ⟨a, ha, b, hb, subset.trans h xy⟩, + inter_sets := assume x y ⟨a, ha, b, hb, hx⟩ ⟨c, hc, d, hd, hy⟩, + ⟨_, inter_mem_sets ha hc, _, inter_mem_sets hb hd, + calc a ∩ c ∩ (b ∩ d) = (a ∩ b) ∩ (c ∩ d) : by ac_refl + ... ⊆ x ∩ y : inter_subset_inter hx hy⟩ }⟩ @[simp] lemma mem_inf_sets {f g : filter α} {s : set α} : s ∈ (f ⊓ g).sets ↔ ∃t₁∈f.sets, ∃t₂∈g.sets, t₁ ∩ t₂ ⊆ s := iff.rfl @@ -305,7 +307,7 @@ instance complete_lattice_filter : complete_lattice (filter α) := /- lattice equations -/ lemma empty_in_sets_eq_bot {f : filter α} : ∅ ∈ f.sets ↔ f = ⊥ := -⟨assume h, bot_unique $ assume s _, f.upwards_sets h (empty_subset s), +⟨assume h, bot_unique $ assume s _, mem_sets_of_superset h (empty_subset s), assume : f = ⊥, this.symm ▸ mem_bot_sets⟩ lemma inhabited_of_mem_sets {f : filter α} {s : set α} (hf : f ≠ ⊥) (hs : s ∈ f.sets) : @@ -331,11 +333,16 @@ by filter_upwards [hs₁] assume a ha, classical.by_contradiction $ assume ha', lemma infi_sets_eq {f : ι → filter α} (h : directed (≤) f) (ne : nonempty ι) : (infi f).sets = (⋃ i, (f i).sets) := let ⟨i⟩ := ne, u := { filter . - sets := (⋃ i, (f i).sets), - exists_mem_sets := ⟨univ, begin simp, exact ⟨i, univ_mem_sets⟩ end⟩, - directed_sets := directed_on_Union (show directed (≤) f, from h) (assume i, (f i).directed_sets), - upwards_sets := by simpa using assume x y j xf (xy : x ⊆ y), - exists.intro j ((f j).upwards_sets xf xy) } in + sets := (⋃ i, (f i).sets), + univ_sets := begin simp, exact ⟨i, univ_mem_sets⟩ end, + sets_of_superset := begin simp, assume x y i hx hxy, exact ⟨i, mem_sets_of_superset hx hxy⟩ end, + inter_sets := + begin + simp, + assume x y a hx b hy, + rcases h a b with ⟨c, ha, hb⟩, + exact ⟨c, inter_mem_sets (ha hx) (hb hy)⟩ + end } in subset.antisymm (show u ≤ infi f, from le_infi $ assume i, le_supr (λi, (f i).sets) i) (Union_subset $ assume i, infi_le f i) @@ -381,11 +388,11 @@ instance : bounded_distrib_lattice (filter α) := simp only [and_assoc, mem_inf_sets, mem_sup_sets, exists_prop, exists_imp_distrib, and_imp], intros hs t₁ ht₁ t₂ ht₂ hts, exact ⟨s ∪ t₁, - x.upwards_sets hs $ subset_union_left _ _, - y.upwards_sets ht₁ $ subset_union_right _ _, + x.sets_of_superset hs $ subset_union_left _ _, + y.sets_of_superset ht₁ $ subset_union_right _ _, s ∪ t₂, - x.upwards_sets hs $ subset_union_left _ _, - z.upwards_sets ht₂ $ subset_union_right _ _, + x.sets_of_superset hs $ subset_union_left _ _, + z.sets_of_superset ht₂ $ subset_union_right _ _, subset.trans (@le_sup_inf (set α) _ _ _ _) (union_subset (subset.refl _) hts)⟩ end, ..filter.complete_lattice_filter } @@ -474,11 +481,10 @@ section map /-- The forward map of a filter -/ def map (m : α → β) (f : filter α) : filter β := -{ sets := preimage m ⁻¹' f.sets, - exists_mem_sets := ⟨univ, univ_mem_sets⟩, - upwards_sets := assume s t hs st, f.upwards_sets hs (assume x h, st h), - directed_sets := assume s hs t ht, ⟨s ∩ t, inter_mem_sets hs ht, - inter_subset_left _ _, inter_subset_right _ _⟩ } +{ sets := preimage m ⁻¹' f.sets, + univ_sets := univ_mem_sets, + sets_of_superset := assume s t hs st, mem_sets_of_superset hs $ preimage_mono st, + inter_sets := assume s t hs ht, inter_mem_sets hs ht } @[simp] lemma map_principal {s : set α} {f : α → β} : map f (principal s) = principal (set.image f s) := @@ -489,7 +495,7 @@ variables {f : filter α} {m : α → β} {m' : β → γ} {s : set α} {t : set @[simp] lemma mem_map : t ∈ (map m f).sets ↔ {x | m x ∈ t} ∈ f.sets := iff.rfl lemma image_mem_map (hs : s ∈ f.sets) : m '' s ∈ (map m f).sets := -f.upwards_sets hs $ assume x hx, ⟨x, hx, rfl⟩ +f.sets_of_superset hs $ subset_preimage_image m s @[simp] lemma map_id : filter.map id f = f := filter_eq $ rfl @@ -506,27 +512,24 @@ section vmap /-- The inverse map of a filter -/ def vmap (m : α → β) (f : filter β) : filter α := -{ sets := { s | ∃t∈f.sets, m ⁻¹' t ⊆ s }, - exists_mem_sets := ⟨univ, univ, univ_mem_sets, by simp⟩, - upwards_sets := assume a b ⟨a', ha', ma'a⟩ ab, ⟨a', ha', subset.trans ma'a ab⟩, - directed_sets := assume a ⟨a', ha₁, ha₂⟩ b ⟨b', hb₁, hb₂⟩, - ⟨preimage m (a' ∩ b'), - ⟨a' ∩ b', inter_mem_sets ha₁ hb₁, subset.refl _⟩, - subset.trans (preimage_mono $ inter_subset_left _ _) ha₂, - subset.trans (preimage_mono $ inter_subset_right _ _) hb₂⟩ } +{ sets := { s | ∃t∈f.sets, m ⁻¹' t ⊆ s }, + univ_sets := ⟨univ, univ_mem_sets, by simp⟩, + sets_of_superset := assume a b ⟨a', ha', ma'a⟩ ab, + ⟨a', ha', subset.trans ma'a ab⟩, + inter_sets := assume a b ⟨a', ha₁, ha₂⟩ ⟨b', hb₁, hb₂⟩, + ⟨a' ∩ b', inter_mem_sets ha₁ hb₁, inter_subset_inter ha₂ hb₂⟩ } end vmap /-- The cofinite filter is the filter of subsets whose complements are finite. -/ def cofinite : filter α := -{ sets := {s | finite (- s)}, - exists_mem_sets := ⟨univ, by simp⟩, - upwards_sets := assume s t, assume hs : finite (-s), assume st: s ⊆ t, +{ sets := {s | finite (- s)}, + univ_sets := by simp, + sets_of_superset := assume s t (hs : finite (-s)) (st: s ⊆ t), finite_subset hs $ @lattice.neg_le_neg (set α) _ _ _ st, - directed_sets := assume s, assume hs : finite (-s), assume t, assume ht : finite (-t), - ⟨s ∩ t, by simp [compl_inter, finite_union, ht, hs], - inter_subset_left _ _, inter_subset_right _ _⟩ } + inter_sets := assume s t (hs : finite (-s)) (ht : finite (-t)), + by simp [compl_inter, finite_union, ht, hs] } /-- The monadic bind operation on filter is defined the usual way in terms of `map` and `join`. -/ @@ -565,7 +568,7 @@ theorem preimage_mem_vmap (ht : t ∈ g.sets) : m ⁻¹' t ∈ (vmap m g).sets : ⟨t, ht, subset.refl _⟩ lemma vmap_id : vmap id f = f := -le_antisymm (assume s, preimage_mem_vmap) (assume s ⟨t, ht, hst⟩, f.upwards_sets ht hst) +le_antisymm (assume s, preimage_mem_vmap) (assume s ⟨t, ht, hst⟩, mem_sets_of_superset ht hst) lemma vmap_vmap_comp {m : γ → β} {n : β → α} : vmap m (vmap n f) = vmap (n ∘ m) f := le_antisymm @@ -579,7 +582,7 @@ filter_eq $ set.ext $ assume s, assume : preimage m t ⊆ s, ⟨t, subset.refl t, this⟩⟩ lemma map_le_iff_le_vmap : map m f ≤ g ↔ f ≤ vmap m g := -⟨assume h s ⟨t, ht, hts⟩, f.upwards_sets (h ht) hts, assume h s ht, h ⟨_, ht, subset.refl _⟩⟩ +⟨assume h s ⟨t, ht, hts⟩, mem_sets_of_superset (h ht) hts, assume h s ht, h ⟨_, ht, subset.refl _⟩⟩ lemma gc_map_vmap (m : α → β) : galois_connection (map m) (vmap m) := assume f g, map_le_iff_le_vmap @@ -609,7 +612,7 @@ lemma vmap_sup : vmap m (g₁ ⊔ g₂) = vmap m g₁ ⊔ vmap m g₂ := le_antisymm (assume s ⟨⟨t₁, ht₁, hs₁⟩, ⟨t₂, ht₂, hs₂⟩⟩, ⟨t₁ ∪ t₂, - ⟨g₁.upwards_sets ht₁ (subset_union_left _ _), g₂.upwards_sets ht₂ (subset_union_right _ _)⟩, + ⟨g₁.sets_of_superset ht₁ (subset_union_left _ _), g₂.sets_of_superset ht₂ (subset_union_right _ _)⟩, union_subset hs₁ hs₂⟩) (sup_le (vmap_mono le_sup_left) (vmap_mono le_sup_right)) @@ -630,7 +633,7 @@ have ∀s, preimage m (image m s) = s, le_antisymm (assume s hs, ⟨ image m s, - f.upwards_sets hs $ by simp [this, subset.refl], + f.sets_of_superset hs $ by simp [this, subset.refl], by simp [this, subset.refl]⟩) le_vmap_map @@ -691,7 +694,7 @@ begin filter_upwards [h, hs], simp [subset_def] {contextual := tt} end, -le_antisymm (this m₁ m₂ h) (this m₂ m₁ $ f.upwards_sets h $ assume x, eq.symm) +le_antisymm (this m₁ m₂ h) (this m₂ m₁ $ mem_sets_of_superset h $ assume x, eq.symm) -- this is a generic rule for monotone functions: lemma map_infi_le {f : ι → filter α} {m : α → β} : @@ -744,7 +747,7 @@ map_inf' univ_mem_sets univ_mem_sets (assume x _ y _, h x y) lemma map_eq_vmap_of_inverse {f : filter α} {m : α → β} {n : β → α} (h₁ : m ∘ n = id) (h₂ : n ∘ m = id) : map m f = vmap n f := le_antisymm - (assume b ⟨a, ha, (h : preimage n a ⊆ b)⟩, f.upwards_sets ha $ + (assume b ⟨a, ha, (h : preimage n a ⊆ b)⟩, f.sets_of_superset ha $ calc a = preimage (n ∘ m) a : by simp [h₂, preimage_id] ... ⊆ preimage m b : preimage_mono h) (assume b (hb : preimage m b ∈ f.sets), @@ -798,7 +801,7 @@ classical.by_cases by rw [infi_sets_eq hd this] at he; simp at he; assumption, let ⟨i, hi⟩ := this in hb i $ bot_unique $ - assume s _, (f i).upwards_sets hi $ empty_subset _) + assume s _, (f i).sets_of_superset hi $ empty_subset _) (assume : ¬ nonempty ι, have univ ⊆ (∅ : set α), begin @@ -993,7 +996,7 @@ lemma map_lift_eq2 {g : set β → filter γ} {m : α → β} (hg : monotone g) le_antisymm (infi_le_infi2 $ assume s, ⟨image m s, infi_le_infi2 $ assume hs, ⟨ - f.upwards_sets hs $ assume a h, mem_image_of_mem _ h, + f.sets_of_superset hs $ assume a h, mem_image_of_mem _ h, le_refl _⟩⟩) (infi_le_infi2 $ assume t, ⟨preimage m t, infi_le_infi2 $ assume ht, ⟨ht, @@ -1301,7 +1304,7 @@ lemma prod_map_map_eq {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ le_antisymm (assume s hs, let ⟨s₁, hs₁, s₂, hs₂, h⟩ := mem_prod_iff.mp hs in - filter.upwards_sets _ (prod_mem_prod (image_mem_map hs₁) (image_mem_map hs₂)) $ + filter.sets_of_superset _ (prod_mem_prod (image_mem_map hs₁) (image_mem_map hs₂)) $ calc set.prod (m₁ '' s₁) (m₂ '' s₂) = (λp:α₁×α₂, (m₁ p.1, m₂ p.2)) '' set.prod s₁ s₂ : set.prod_image_image_eq ... ⊆ _ : by rwa [image_subset_iff]) @@ -1457,7 +1460,7 @@ lemma ultrafilter_pure {a : α} : ultrafilter (pure a) := simp only [classical.not_forall, not_imp, exists_imp_distrib, singleton_subset_iff], exact assume s ⟨hs, hna⟩, have {a} ∩ s ∈ g.sets, from inter_mem_sets ‹{a} ∈ g.sets› hs, - have ∅ ∈ g.sets, from g.upwards_sets this $ + have ∅ ∈ g.sets, from mem_sets_of_superset this $ assume x ⟨hxa, hxs⟩, begin simp at hxa; simp [hxa] at hxs, exact hna hxs end, have g = ⊥, from empty_in_sets_eq_bot.mp this, hg this diff --git a/order/liminf_limsup.lean b/order/liminf_limsup.lean index aebd1c2b9a2f0..f121ffba441ab 100644 --- a/order/liminf_limsup.lean +++ b/order/liminf_limsup.lean @@ -54,7 +54,7 @@ bounded. -/ lemma is_bounded_iff : f.is_bounded r ↔ (∃s∈f.sets, ∃b, s ⊆ {x | r x b}) := iff.intro (assume ⟨b, hb⟩, ⟨{a | r a b}, hb, b, subset.refl _⟩) - (assume ⟨s, hs, b, hb⟩, ⟨b, f.upwards_sets hs hb⟩) + (assume ⟨s, hs, b, hb⟩, ⟨b, mem_sets_of_superset hs hb⟩) /-- A bounded function `u` is in particular eventually bounded. -/ lemma is_bounded_under_of {f : filter β} {u : β → α} : @@ -74,15 +74,15 @@ lemma is_bounded_sup [is_trans α r] (hr : ∀b₁ b₂, ∃b, r b₁ b ∧ r b is_bounded r f → is_bounded r g → is_bounded r (f ⊔ g) | ⟨b₁, h₁⟩ ⟨b₂, h₂⟩ := let ⟨b, rb₁b, rb₂b⟩ := hr b₁ b₂ in ⟨b, mem_sup_sets.2 ⟨ - f.upwards_sets h₁ $ assume x rxb₁, show r x b, from trans rxb₁ rb₁b, - g.upwards_sets h₂ $ assume x rxb₂, show r x b, from trans rxb₂ rb₂b⟩⟩ + mem_sets_of_superset h₁ $ assume x rxb₁, show r x b, from trans rxb₁ rb₁b, + mem_sets_of_superset h₂ $ assume x rxb₂, show r x b, from trans rxb₂ rb₂b⟩⟩ lemma is_bounded_of_le (h : f ≤ g) : is_bounded r g → is_bounded r f | ⟨b, hb⟩ := ⟨b, h hb⟩ lemma is_bounded_under_of_is_bounded {q : β → β → Prop} {u : α → β} (hf : ∀a₀ a₁, r a₀ a₁ → q (u a₀) (u a₁)) : f.is_bounded r → f.is_bounded_under q u -| ⟨b, h⟩ := ⟨u b, show {x : α | q (u x) (u b)} ∈ f.sets, from f.upwards_sets h $ assume a, hf _ _⟩ +| ⟨b, h⟩ := ⟨u b, show {x : α | q (u x) (u b)} ∈ f.sets, from mem_sets_of_superset h $ assume a, hf _ _⟩ /-- `is_cobounded (≺) f` states that filter `f` is not tend to infinite w.r.t. `≺`. This is also called frequently bounded. Will be usually instantiated with `≤` or `≥`.