refactor(order/filter): simplify filter structure

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

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⟩

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')) :

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,

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 = (⨅b<a, principal {c | b < c}) ⊓ (⨅b>a, 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. -/