chore(order/filter): simplify definition of filter.prod; cleanup

Author: johoelzl

analysis/ennreal.lean

@@ -630,7 +630,7 @@ begin
   apply tendsto_principal.2 _,
   revert b,
   simp [forall_ennreal],
-  exact assume r hr hr', mem_prod_sets.mpr ⟨
+  exact assume r hr hr', mem_prod_iff.mpr ⟨
     {a | of_real r < a}, mem_nhds_sets (is_open_lt' _) hr',
     univ, univ_mem_sets, assume ⟨c, d⟩ ⟨hc, _⟩, lt_of_lt_of_le hc $ le_add_right $ le_refl _⟩
 end,

analysis/real.lean

@@ -116,7 +116,7 @@ real.uniform_continuous_abs.continuous
 
 lemma rat.uniform_continuous_abs : uniform_continuous (abs : ℚ → ℚ) :=
 uniform_continuous_of_metric.2 $ λ ε ε0,
-  ⟨ε, ε0, λ a b h, lt_of_le_of_lt 
+  ⟨ε, ε0, λ a b h, lt_of_le_of_lt
     (by simpa [rat.dist_eq] using abs_abs_sub_abs_le_abs_sub _ _) h⟩
 
 lemma rat.continuous_abs : continuous (abs : ℚ → ℚ) :=
@@ -285,7 +285,7 @@ begin
     rcases Cauchy.mem_uniformity'.1 hs with ⟨t, tu, ts⟩,
     apply ts,
     rcases comp_mem_uniformity_sets tu with ⟨d, du, dt⟩,
-    refine mem_prod_sets.2
+    refine mem_prod_iff.2
       ⟨_, le_nhds_lim_of_cauchy f.2 (mem_nhds_right (lim f.1) du),
        _, le_nhds_lim_of_cauchy g.2 (mem_nhds_left (lim g.1) du), λ x h, _⟩,
     cases x with a b, cases h with h₁ h₂,
@@ -296,7 +296,7 @@ begin
     rcases mem_uniformity_is_closed tu with ⟨d, du, dc, dt⟩,
     refine H {p | (lim p.1.1, lim p.2.1) ∈ t}
       (Cauchy.mem_uniformity'.2 ⟨d, du, λ f g h, _⟩),
-    rcases mem_prod_sets.1 h with ⟨x, xf, y, yg, h⟩,
+    rcases mem_prod_iff.1 h with ⟨x, xf, y, yg, h⟩,
     have limc : ∀ (f : Cauchy ℝ) (x ∈ f.1.sets), lim f.1 ∈ closure x,
     { intros f x xf,
       rw closure_eq_nhds,

analysis/topology/continuity.lean

@@ -376,6 +376,9 @@ lemma is_open_prod {s : set α} {t : set β} (hs : is_open s) (ht : is_open t) :
   is_open (set.prod s t) :=
 is_open_inter (continuous_fst s hs) (continuous_snd t ht)
 
+lemma nhds_prod_eq {a : α} {b : β} : nhds (a, b) = filter.prod (nhds a) (nhds b) :=
+by rw [filter.prod, prod.topological_space, nhds_sup, nhds_induced_eq_vmap, nhds_induced_eq_vmap]
+
 lemma prod_generate_from_generate_from_eq {s : set (set α)} {t : set (set β)}
   (hs : ⋃₀ s = univ) (ht : ⋃₀ t = univ) :
   @prod.topological_space α β (generate_from s) (generate_from t) =
@@ -416,32 +419,11 @@ le_antisymm
       this ▸ (generate_open.basic _ ⟨univ, t, is_open_univ, ht, rfl⟩)))
   (generate_from_le $ assume g ⟨s, t, hs, ht, g_eq⟩, g_eq.symm ▸ is_open_prod hs ht)
 
-lemma nhds_prod_eq {a : α} {b : β} : nhds (a, b) = filter.prod (nhds a) (nhds b) :=
-by rw [prod_eq_generate_from, nhds_generate_from];
-  exact le_antisymm
-    (le_infi $ assume s, le_infi $ assume hs, le_infi $ assume t, le_infi $ assume ht,
-      begin
-        simp [mem_nhds_sets_iff] at hs, simp [mem_nhds_sets_iff] at ht,
-        rcases hs with ⟨s', hs_sub, hs', as'⟩,
-        rcases ht with ⟨t', ht_sub, ht', at'⟩,
-        exact infi_le_of_le (set.prod s' t')
-          (infi_le_of_le ⟨⟨as', at'⟩, s', t', hs', ht', rfl⟩ $
-          principal_mono.mpr $ set.prod_mono hs_sub ht_sub)
-      end)
-    (le_infi $ assume s, le_infi $ assume ⟨hab, s', t', hs', ht', s_eq⟩,
-      begin
-        revert hab,
-        simp [s_eq],
-        exact assume ha hb, @prod_mem_prod α β s' t' (nhds a) (nhds b)
-          (mem_nhds_sets_iff.mpr ⟨s', subset.refl s', hs', ha⟩)
-          (mem_nhds_sets_iff.mpr ⟨t', subset.refl t', ht', hb⟩)
-      end)
-
 lemma is_open_prod_iff {s : set (α×β)} : is_open s ↔
   (∀a b, (a, b) ∈ s → ∃u v, is_open u ∧ is_open v ∧ a ∈ u ∧ b ∈ v ∧ set.prod u v ⊆ s) :=
 begin
   rw [is_open_iff_nhds],
-  simp [nhds_prod_eq, mem_prod_sets],
+  simp [nhds_prod_eq, mem_prod_iff],
   simp [mem_nhds_sets_iff],
   exact forall_congr (assume a, ball_congr $ assume b h,
     ⟨assume ⟨u', ⟨u, us, uo, au⟩, v', ⟨v, vs, vo, bv⟩, h⟩,

analysis/topology/topological_space.lean

@@ -894,6 +894,12 @@ le_antisymm
       end)
   end
 
+lemma nhds_sup {t₁ t₂ : topological_space α} {a : α} :
+  @nhds α (t₁ ⊔ t₂) a = @nhds α t₁ a ⊓ @nhds α t₂ a :=
+calc @nhds α (t₁ ⊔ t₂) a = @nhds α (⨆b:bool, cond b t₁ t₂) a : by rw [supr_bool_eq]
+  ... = (⨅b, @nhds α (cond b t₁ t₂) a) : begin rw [nhds_supr] end
+  ... = @nhds α t₁ a ⊓ @nhds α t₂ a : by rw [infi_bool_eq]
+
 end
 
 end constructions
@@ -943,7 +949,7 @@ lemma is_topological_basis_of_open_of_nhds {s : set (set α)}
       (is_open_inter _ _ _ (h_open _ ht₁) (h_open _ ht₂)),
   eq_univ_iff_forall.2 $ assume a,
     let ⟨u, h₁, h₂, _⟩ := h_nhds a univ trivial (is_open_univ _) in
-    ⟨u, h₁, h₂⟩, 
+    ⟨u, h₁, h₂⟩,
   le_antisymm
     (assume u hu,
       (@is_open_iff_nhds α (generate_from _) _).mpr $ assume a hau,

analysis/topology/uniform_space.lean

@@ -78,8 +78,10 @@ def uniform_space.core.mk' {α : Type u} (U : filter (α × α))
   (symm : ∀ r ∈ U.sets, {p | prod.swap p ∈ r} ∈ U.sets)
   (comp : ∀ r ∈ U.sets, ∃ t ∈ U.sets, comp_rel t t ⊆ r) : uniform_space.core α :=
 ⟨U, λ r ru, id_rel_subset.2 (refl _ ru), symm,
-  λ r ru, begin
-    rw [mem_lift'_sets], exact comp _ ru,
+  begin
+    intros r ru,
+    rw [mem_lift'_sets],
+    exact comp _ ru,
     apply monotone_comp_rel; exact monotone_id,
   end⟩
 
@@ -88,10 +90,10 @@ def uniform_space.core.to_topological_space {α : Type u} (u : uniform_space.cor
   topological_space α :=
 { is_open        := λs, ∀x∈s, { p : α × α | p.1 = x → p.2 ∈ s } ∈ u.uniformity.sets,
   is_open_univ   := by simp; intro; exact univ_mem_sets,
-  is_open_inter  := assume s t hs ht x ⟨xs, xt⟩,
-    u.uniformity.upwards_sets (inter_mem_sets (hs x xs) (ht x xt)) $ assume p ⟨ps, pt⟩ h, ⟨ps h, pt h⟩,
-  is_open_sUnion := assume s hs x ⟨t, ts, xt⟩,
-    u.uniformity.upwards_sets (hs t ts x xt) $ assume p ph h, ⟨t, ts, ph h⟩ }
+  is_open_inter  :=
+    assume s t hs ht x ⟨xs, xt⟩, by filter_upwards [hs x xs, ht x xt]; simp {contextual := tt},
+  is_open_sUnion :=
+    assume s hs x ⟨t, ts, xt⟩, by filter_upwards [hs t ts x xt] assume p ph h, ⟨t, ts, ph h⟩ }
 
 lemma uniform_space.core_eq : ∀{u₁ u₂ : uniform_space.core α}, u₁.uniformity = u₂.uniformity → u₁ = u₂
 | ⟨u₁, _, _, _⟩  ⟨u₂, _, _, _⟩ h := have u₁ = u₂, from h, by simp [*]
@@ -188,22 +190,19 @@ let ⟨t, ht₁, ht₂⟩ := comp_mem_uniformity_sets hs in
 let ⟨t', ht', ht'₁, ht'₂⟩ := symm_of_uniformity ht₁ in
 ⟨t', ht', ht'₁, subset.trans (monotone_comp_rel monotone_id monotone_id ht'₂) ht₂⟩
 
-lemma uniformity_le_symm : uniformity ≤ map (@prod.swap α α) uniformity :=
-calc uniformity = id <$> uniformity : (functor.id_map _).symm
-  ... = (@prod.swap α α ∘ prod.swap) <$> uniformity :
-    congr_arg (λf : (α×α)→(α×α), f <$> uniformity) (by funext x; cases x; refl)
-  ... = (map prod.swap ∘ map prod.swap) uniformity :
-    congr map_compose rfl
-  ... ≤ (@prod.swap α α) <$> uniformity : map_mono symm_le_uniformity
+lemma uniformity_le_symm : uniformity ≤ (@prod.swap α α) <$> uniformity :=
+by rw [map_swap_eq_vmap_swap];
+from map_le_iff_le_vmap.1 tendsto_swap_uniformity
 
 lemma uniformity_eq_symm : uniformity = (@prod.swap α α) <$> uniformity :=
 le_antisymm uniformity_le_symm symm_le_uniformity
 
 theorem uniformity_lift_le_swap {g : set (α×α) → filter β} {f : filter β} (hg : monotone g)
   (h : uniformity.lift (λs, g (preimage prod.swap s)) ≤ f) : uniformity.lift g ≤ f :=
-le_trans
-  (lift_mono uniformity_le_symm (le_refl _))
-  (by rw [map_lift_eq2 hg, image_swap_eq_preimage_swap]; exact h)
+calc uniformity.lift g ≤ (filter.map prod.swap (@uniformity α _)).lift g :
+    lift_mono uniformity_le_symm (le_refl _)
+  ... ≤ _ :
+    by rw [map_lift_eq2 hg, image_swap_eq_preimage_swap]; exact h
 
 lemma uniformity_lift_le_comp {f : set (α×α) → filter β} (h : monotone f):
   uniformity.lift (λs, f (comp_rel s s)) ≤ uniformity.lift f :=
@@ -238,25 +237,21 @@ lemma mem_nhds_uniformity_iff {x : α} {s : set α} :
   (s ∈ (nhds x).sets) ↔ ({p : α × α | p.1 = x → p.2 ∈ s} ∈ (@uniformity α _).sets) :=
 ⟨ begin
     simp [mem_nhds_sets_iff, is_open_uniformity],
-    exact assume t ts ht xt, uniformity.upwards_sets (ht x xt) $ assume ⟨x', y⟩ h eq, ts $ h eq
+    exact assume t ts ht xt, by filter_upwards [ht x xt] assume ⟨x', y⟩ h eq, ts $ h eq
   end,
 
   assume hs,
   mem_nhds_sets_iff.mpr ⟨{x | {p : α × α | p.1 = x → p.2 ∈ s} ∈ (@uniformity α _).sets},
-    assume x', assume hx' : {p : α × α | p.fst = x' → p.snd ∈ s} ∈ (@uniformity α _).sets,
-      refl_mem_uniformity hx' rfl,
+    assume x' hx', refl_mem_uniformity hx' rfl,
     is_open_uniformity.mpr $ assume x' hx',
       let ⟨t, ht, tr⟩ := comp_mem_uniformity_sets hx' in
-      uniformity.upwards_sets ht $
-      assume ⟨a, b⟩ hp' (eq : a = x'),
-      have hp : (x', b) ∈ t, from eq ▸ hp',
-      show {p : α × α | p.fst = b → p.snd ∈ s} ∈ (@uniformity α _).sets,
-        from uniformity.upwards_sets ht $
-          assume ⟨a, b'⟩ hp' (heq : a = b),
-          have (b, b') ∈ t, from heq ▸ hp',
-          have (x', b') ∈ comp_rel t t, from ⟨b, hp, this⟩,
-          show b' ∈ s,
-            from tr this rfl,
+      by filter_upwards [ht] assume ⟨a, b⟩ hp' (hax' : a = x'),
+      by filter_upwards [ht] assume ⟨a, b'⟩ hp'' (hab : a = b),
+      have hp : (x', b) ∈ t, from hax' ▸ hp',
+      have (b, b') ∈ t, from hab ▸ hp'',
+      have (x', b') ∈ comp_rel t t, from ⟨b, hp, this⟩,
+      show b' ∈ s,
+        from tr this rfl,
     hs⟩⟩
 
 lemma nhds_eq_vmap_uniformity {x : α} : nhds x = uniformity.vmap (prod.mk x) :=
@@ -314,8 +309,9 @@ lemma nhds_nhds_eq_uniformity_uniformity_prod {a b : α} :
   filter.prod (nhds a) (nhds b) =
   uniformity.lift (λs:set (α×α), uniformity.lift' (λt:set (α×α),
     set.prod {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t})) :=
-show (nhds a).lift (λs:set α, (nhds b).lift (λt:set α, principal (set.prod s t))) = _,
 begin
+  rw [prod_def],
+  show (nhds a).lift (λs:set α, (nhds b).lift (λt:set α, principal (set.prod s t))) = _,
   rw [lift_nhds_right],
   apply congr_arg, funext s,
   rw [lift_nhds_left],
@@ -387,7 +383,7 @@ calc (a, b) ∈ closure t ↔ (nhds (a, b) ⊓ principal t ≠ ⊥) : by simp [c
 
 lemma uniformity_eq_uniformity_closure : (@uniformity α _) = uniformity.lift' closure :=
 le_antisymm
-  (le_infi $ assume s, le_infi $ assume hs, by simp; exact uniformity.upwards_sets hs subset_closure)
+  (le_infi $ assume s, le_infi $ assume hs, by simp; filter_upwards [hs] subset_closure)
   (calc uniformity.lift' closure ≤ uniformity.lift' (λd, comp_rel d (comp_rel d d)) :
       lift'_mono' (by intros s hs; rw [closure_eq_inter_uniformity]; exact bInter_subset_of_mem hs)
     ... ≤ uniformity : comp_le_uniformity3)
@@ -402,8 +398,7 @@ le_antisymm
       calc s ⊆ t : hst
        ... ⊆ interior d : (subset_interior_iff_subset_of_open ht).mpr $
         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,
-      from (@uniformity α _).upwards_sets hs $ this,
+    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)
 
@@ -1084,7 +1079,7 @@ show preimage (λp:(α×α), (ψ p.1, ψ p.2)) d ∈ uniformity.sets,
     from is_open_iff_nhds.mp is_open_interior (x₁, x₂) hx_t,
   have interior t ∈ (filter.prod (nhds x₁) (nhds x₂)).sets,
     by rwa [nhds_prod_eq, le_principal_iff] at this,
-  let ⟨m₁, hm₁, m₂, hm₂, (hm : set.prod m₁ m₂ ⊆ interior t)⟩ := mem_prod_sets.mp this in
+  let ⟨m₁, hm₁, m₂, hm₂, (hm : set.prod m₁ m₂ ⊆ interior t)⟩ := mem_prod_iff.mp this in
   let ⟨a, ha₁, _, ha₂⟩ := h_pnt hm₁ in
   let ⟨b, hb₁, hb₂, _⟩ := h_pnt hm₂ in
   have set.prod (preimage e m₁) (preimage e m₂) ⊆ preimage (λp:(β×β), (f p.1, f p.2)) s,
@@ -1145,9 +1140,9 @@ private lemma comp_rel_gen_gen_subset_gen_comp_rel {s t : set (α×α)} : comp_r
   (gen (comp_rel s t) : set (Cauchy α × Cauchy α)) :=
 assume ⟨f, g⟩ ⟨h, h₁, h₂⟩,
 let ⟨t₁, (ht₁ : t₁ ∈ f.val.sets), t₂, (ht₂ : t₂ ∈ h.val.sets), (h₁ : set.prod t₁ t₂ ⊆ s)⟩ :=
-  mem_prod_sets.mp h₁ in
+  mem_prod_iff.mp h₁ in
 let ⟨t₃, (ht₃ : t₃ ∈ h.val.sets), t₄, (ht₄ : t₄ ∈ g.val.sets), (h₂ : set.prod t₃ t₄ ⊆ t)⟩ :=
-  mem_prod_sets.mp h₂ in
+  mem_prod_iff.mp h₂ in
 have t₂ ∩ t₃ ∈ h.val.sets,
   from inter_mem_sets ht₂ ht₃,
 let ⟨x, xt₂, xt₃⟩ :=
@@ -1225,7 +1220,7 @@ have h_ex : ∀s∈(@uniformity (Cauchy α) _).sets, ∃y:α, (f, pure_cauchy y)
   let ⟨t, ht, (h : set.prod t t ⊆ t')⟩ := mem_prod_same_iff.mp this in
   let ⟨x, (hx : x ∈ t)⟩ := inhabited_of_mem_sets f.property.left ht in
   have t'' ∈ (filter.prod f.val (pure x)).sets,
-    from mem_prod_sets.mpr ⟨t, ht, {y:α | (x, y) ∈ t'},
+    from mem_prod_iff.mpr ⟨t, ht, {y:α | (x, y) ∈ t'},
       assume y, begin simp, intro h, simp [h], exact refl_mem_uniformity ht'₁ end,
       assume ⟨a, b⟩ ⟨(h₁ : a ∈ t), (h₂ : (x, b) ∈ t')⟩,
         ht'₂ $ prod_mk_mem_comp_rel (@h (a, x) ⟨h₁, hx⟩) h₂⟩,
@@ -1551,7 +1546,7 @@ have map (λp:(α×α)×(β×β), ((p.1.1, p.2.1), (p.1.2, p.2.2))) =
   vmap (λp:(α×β)×(α×β), ((p.1.1, p.2.1), (p.1.2, p.2.2))),
   from funext $ assume f, map_eq_vmap_of_inverse
     (funext $ assume ⟨⟨_, _⟩, ⟨_, _⟩⟩, rfl) (funext $ assume ⟨⟨_, _⟩, ⟨_, _⟩⟩, rfl),
-by rw [this, uniformity_prod, prod_def, vmap_inf, vmap_vmap_comp, vmap_vmap_comp]
+by rw [this, uniformity_prod, filter.prod, vmap_inf, vmap_vmap_comp, vmap_vmap_comp]
 
 lemma mem_uniform_prod [t₁ : uniform_space α] [t₂ : uniform_space β] {a : set (α × α)} {b : set (β × β)}
   (ha : a ∈ (@uniformity α _).sets) (hb : b ∈ (@uniformity β _).sets) :

data/analysis/filter.lean

@@ -210,7 +210,7 @@ F'.of_equiv $ show (Σ u:unit, Π (i : α), true → (F i).σ) ≃ Π i, (F i).
 
 /-- Construct a realizer for the product of filters -/
 protected def prod {f g : filter α} (F : f.realizer) (G : g.realizer) : (f.prod g).realizer :=
-of_eq prod_def.symm $ (F.vmap _).inf (G.vmap _)
+(F.vmap _).inf (G.vmap _)
 
 theorem le_iff {f g : filter α} (F : f.realizer) (G : g.realizer) :
   f ≤ g ↔ ∀ b : G.σ, ∃ a : F.σ, F.F a ≤ G.F b :=