chore(topology/*): reverse order on topological and uniform spaces (#1138)

* chore(topology/*): reverse order on topological and uniform spaces

* fix(topology/order): private lemma hiding partial order oscillation,
following Mario's suggestion

* change a temporary name

Co-Authored-By: Johan Commelin <johan@commelin.net>

* forgotten rename

Author: PatrickMassot

src/measure_theory/borel_space.lean

@@ -294,15 +294,15 @@ measurable.is_glb hf $ λ b, is_glb_infi
 
 lemma measurable.supr_Prop {α} [topological_space α] [complete_linear_order α]
   [orderable_topology α] [second_countable_topology α]
-  {β} [measurable_space β] {p : Prop} {f : β → α} (hf : measurable f): 
+  {β} [measurable_space β] {p : Prop} {f : β → α} (hf : measurable f):
   measurable (λ b, ⨆ h : p, f b) :=
 classical.by_cases
   (assume h : p, begin convert hf, funext, exact supr_pos h end)
   (assume h : ¬p, begin convert measurable_const, funext, exact supr_neg h end)
 
 lemma measurable.infi_Prop {α} [topological_space α] [complete_linear_order α]
   [orderable_topology α] [second_countable_topology α]
-  {β} [measurable_space β] {p : Prop} {f : β → α} (hf : measurable f): 
+  {β} [measurable_space β] {p : Prop} {f : β → α} (hf : measurable f):
   measurable (λ b, ⨅ h : p, f b) :=
 classical.by_cases
   (assume h : p, begin convert hf, funext, exact infi_pos h end )
@@ -352,17 +352,17 @@ end
 end real
 
 namespace nnreal
-open filter measure_theory 
+open filter measure_theory
 
-lemma measurable_add [measurable_space α] {f : α → nnreal} {g : α → nnreal} : 
+lemma measurable_add [measurable_space α] {f : α → nnreal} {g : α → nnreal} :
   measurable f → measurable g → measurable (λa, f a + g a) :=
 measurable_of_continuous2 continuous_add'
 
-lemma measurable_sub [measurable_space α] {f g: α → nnreal} 
-  (hf : measurable f) (hg : measurable g) : measurable (λ a, f a - g a) := 
+lemma measurable_sub [measurable_space α] {f g: α → nnreal}
+  (hf : measurable f) (hg : measurable g) : measurable (λ a, f a - g a) :=
 measurable_of_continuous2 continuous_sub' hf hg
 
-lemma measurable_mul [measurable_space α] {f : α → nnreal} {g : α → nnreal} : 
+lemma measurable_mul [measurable_space α] {f : α → nnreal} {g : α → nnreal} :
   measurable f → measurable g → measurable (λa, f a * g a) :=
 measurable_of_continuous2 continuous_mul'
 
@@ -467,14 +467,14 @@ begin
   { simp [measurable_const] }
 end
 
-lemma measurable_sub {α : Type*} [measurable_space α] {f g : α → ennreal} : 
+lemma measurable_sub {α : Type*} [measurable_space α] {f g : α → ennreal} :
   measurable f → measurable g → measurable (λa, f a - g a) :=
 begin
   refine measurable_of_measurable_nnreal_nnreal (has_sub.sub) _ _ _,
   { simp only [ennreal.coe_sub.symm],
-    exact measurable_coe.comp 
+    exact measurable_coe.comp
       (nnreal.measurable_sub (measurable_fst measurable_id) (measurable_snd measurable_id)) },
-  { simp [measurable_const] }, 
+  { simp [measurable_const] },
   { simp [measurable_const] }
 end
 

src/order/complete_lattice.lean

@@ -584,10 +584,16 @@ eq.trans supr_union $ congr_arg (λx:α, x ⊔ (⨆x∈s, f x)) supr_supr_eq_lef
 show (⨅ x ∈ insert b (∅ : set β), f x) = f b,
   by simp
 
+@[simp] theorem infi_pair {f : β → α} {a b : β} : (⨅ x ∈ ({a, b} : set β), f x) = f a ⊓ f b :=
+by { rw [show {a, b} = (insert b {a} : set β), from rfl, infi_insert, inf_comm], simp }
+
 @[simp] theorem supr_singleton {f : β → α} {b : β} : (⨆ x ∈ (singleton b : set β), f x) = f b :=
 show (⨆ x ∈ insert b (∅ : set β), f x) = f b,
   by simp
 
+@[simp] theorem supr_pair {f : β → α} {a b : β} : (⨆ x ∈ ({a, b} : set β), f x) = f a ⊔ f b :=
+by { rw [show {a, b} = (insert b {a} : set β), from rfl, supr_insert, sup_comm], simp }
+
 lemma infi_image {γ} {f : β → γ} {g : γ → α} {t : set β} :
   (⨅ c ∈ f '' t, g c) = (⨅ b ∈ t, g (f b)) :=
 le_antisymm

src/topology/Top/adjunctions.lean

@@ -15,19 +15,19 @@ namespace Top
 def adj₁ : discrete ⊣ forget :=
 { hom_equiv := λ X Y,
   { to_fun := λ f, f,
-    inv_fun := λ f, ⟨f, continuous_top⟩,
+    inv_fun := λ f, ⟨f, continuous_bot⟩,
     left_inv := by tidy,
     right_inv := by tidy },
   unit := { app := λ X, id },
-  counit := { app := λ X, ⟨id, continuous_top⟩ } }
+  counit := { app := λ X, ⟨id, continuous_bot⟩ } }
 
 def adj₂ : forget ⊣ trivial :=
 { hom_equiv := λ X Y,
-  { to_fun := λ f, ⟨f, continuous_bot⟩,
+  { to_fun := λ f, ⟨f, continuous_top⟩,
     inv_fun := λ f, f,
     left_inv := by tidy,
     right_inv := by tidy },
-  unit := { app := λ X, ⟨id, continuous_bot⟩ },
+  unit := { app := λ X, ⟨id, continuous_top⟩ },
   counit := { app := λ X, id } }
 
 end Top

src/topology/Top/basic.lean

@@ -24,11 +24,11 @@ def of (X : Type u) [topological_space X] : Top := ⟨X⟩
 abbreviation forget : Top.{u} ⥤ Type u := forget
 
 def discrete : Type u ⥤ Top.{u} :=
-{ obj := λ X, ⟨X, ⊤⟩,
-  map := λ X Y f, ⟨f, continuous_top⟩ }
-
-def trivial : Type u ⥤ Top.{u} :=
 { obj := λ X, ⟨X, ⊥⟩,
   map := λ X Y f, ⟨f, continuous_bot⟩ }
 
+def trivial : Type u ⥤ Top.{u} :=
+{ obj := λ X, ⟨X, ⊤⟩,
+  map := λ X Y f, ⟨f, continuous_top⟩ }
+
 end Top

src/topology/Top/limits.lean

@@ -17,15 +17,15 @@ namespace Top
 variables {J : Type u} [small_category J]
 
 def limit (F : J ⥤ Top.{u}) : cone F :=
-{ X := ⟨limit (F ⋙ forget), ⨆ j, (F.obj j).str.induced (limit.π (F ⋙ forget) j)⟩,
+{ X := ⟨limit (F ⋙ forget), ⨅j, (F.obj j).str.induced (limit.π (F ⋙ forget) j)⟩,
   π :=
-  { app := λ j, ⟨limit.π (F ⋙ forget) j, continuous_iff_induced_le.mpr (lattice.le_supr _ j)⟩,
+  { app := λ j, ⟨limit.π (F ⋙ forget) j, continuous_iff_le_induced.mpr (lattice.infi_le _ _)⟩,
     naturality' := λ j j' f, subtype.eq ((limit.cone (F ⋙ forget)).π.naturality f) } }
 
 def limit_is_limit (F : J ⥤ Top.{u}) : is_limit (limit F) :=
-by refine is_limit.of_faithful forget (limit.is_limit _) (λ s, ⟨_, _⟩) (λ s, rfl);
-   exact continuous_iff_le_coinduced.mpr (lattice.supr_le $ λ j,
-     induced_le_iff_le_coinduced.mpr $ continuous_iff_le_coinduced.mp (s.π.app j).property)
+by { refine is_limit.of_faithful forget (limit.is_limit _) (λ s, ⟨_, _⟩) (λ s, rfl),
+     exact continuous_iff_coinduced_le.mpr (lattice.le_infi $ λ j,
+       coinduced_le_iff_le_induced.mp $ continuous_iff_coinduced_le.mp (s.π.app j).property) }
 
 instance Top_has_limits : has_limits.{u} Top.{u} :=
 { has_limits_of_shape := λ J 𝒥,
@@ -38,15 +38,15 @@ instance forget_preserves_limits : preserves_limits (forget : Top.{u} ⥤ Type u
       (limit.is_limit F) (limit.is_limit (F ⋙ forget)) } }
 
 def colimit (F : J ⥤ Top.{u}) : cocone F :=
-{ X := ⟨colimit (F ⋙ forget), ⨅ j, (F.obj j).str.coinduced (colimit.ι (F ⋙ forget) j)⟩,
+{ X := ⟨colimit (F ⋙ forget), ⨆ j, (F.obj j).str.coinduced (colimit.ι (F ⋙ forget) j)⟩,
   ι :=
-  { app := λ j, ⟨colimit.ι (F ⋙ forget) j, continuous_iff_le_coinduced.mpr (lattice.infi_le _ j)⟩,
+  { app := λ j, ⟨colimit.ι (F ⋙ forget) j, continuous_iff_coinduced_le.mpr (lattice.le_supr _ j)⟩,
     naturality' := λ j j' f, subtype.eq ((colimit.cocone (F ⋙ forget)).ι.naturality f) } }
 
 def colimit_is_colimit (F : J ⥤ Top.{u}) : is_colimit (colimit F) :=
-by refine is_colimit.of_faithful forget (colimit.is_colimit _) (λ s, ⟨_, _⟩) (λ s, rfl);
-   exact continuous_iff_induced_le.mpr (lattice.le_infi $ λ j,
-     induced_le_iff_le_coinduced.mpr $ continuous_iff_le_coinduced.mp (s.ι.app j).property)
+by { refine is_colimit.of_faithful forget (colimit.is_colimit _) (λ s, ⟨_, _⟩) (λ s, rfl),
+     exact continuous_iff_le_induced.mpr (lattice.supr_le $ λ j,
+       coinduced_le_iff_le_induced.mp $ continuous_iff_coinduced_le.mp (s.ι.app j).property) }
 
 instance Top_has_colimits : has_colimits.{u} Top.{u} :=
 { has_colimits_of_shape := λ J 𝒥,

src/topology/algebra/ordered.lean

@@ -271,6 +271,14 @@ begin
   letI := induced f ta,
   refine ⟨eq_of_nhds_eq_nhds (λ a, _)⟩,
   rw [nhds_induced_eq_comap, nhds_generate_from, @nhds_eq_orderable β _ _], apply le_antisymm,
+  { refine le_infi (λ s, le_infi $ λ hs, le_principal_iff.2 _),
+    rcases hs with ⟨ab, b, rfl|rfl⟩,
+    { exact mem_comap_sets.2 ⟨{x | f b < x},
+        mem_inf_sets_of_left $ mem_infi_sets _ $ mem_infi_sets (hf.2 ab) $ mem_principal_self _,
+        λ x, hf.1⟩ },
+    { exact mem_comap_sets.2 ⟨{x | x < f b},
+        mem_inf_sets_of_right $ mem_infi_sets _ $ mem_infi_sets (hf.2 ab) $ mem_principal_self _,
+        λ x, hf.1⟩ } },
   { rw [← map_le_iff_le_comap],
     refine le_inf _ _; refine le_infi (λ x, le_infi $ λ h, le_principal_iff.2 _); simp,
     { rcases H₁ h with ⟨b, ab, xb⟩,
@@ -279,14 +287,6 @@ begin
     { rcases H₂ h with ⟨b, ab, xb⟩,
       refine mem_infi_sets _ (mem_infi_sets ⟨ab, b, or.inr rfl⟩ (mem_principal_sets.2 _)),
       exact λ c hc, lt_of_lt_of_le (hf.2 hc) xb } },
-  refine le_infi (λ s, le_infi $ λ hs, le_principal_iff.2 _),
-  rcases hs with ⟨ab, b, rfl|rfl⟩,
-  { exact mem_comap_sets.2 ⟨{x | f b < x},
-      mem_inf_sets_of_left $ mem_infi_sets _ $ mem_infi_sets (hf.2 ab) $ mem_principal_self _,
-      λ x, hf.1⟩ },
-  { exact mem_comap_sets.2 ⟨{x | x < f b},
-      mem_inf_sets_of_right $ mem_infi_sets _ $ mem_infi_sets (hf.2 ab) $ mem_principal_self _,
-      λ x, hf.1⟩ }
 end
 
 theorem induced_orderable_topology {α : Type u} {β : Type v}

src/topology/bases.lean

@@ -40,13 +40,13 @@ let b' := (λf, ⋂₀ f) '' {f:set (set α) | finite f ∧ f ⊆ s ∧ ⋂₀ f
     by rw sInter_empty; exact nonempty_iff_univ_ne_empty.1 ⟨a⟩⟩, sInter_empty⟩, mem_univ _⟩,
  have generate_from s = generate_from b',
     from le_antisymm
-      (generate_from_le $ assume s hs,
+      (le_generate_from $ assume u ⟨t, ⟨hft, htb, ne⟩, eq⟩,
+        eq ▸ @is_open_sInter _ (generate_from s) _ hft (assume s hs, generate_open.basic _ $ htb hs))
+      (le_generate_from $ assume s hs,
         by_cases
           (assume : s = ∅, by rw [this]; apply @is_open_empty _ _)
           (assume : s ≠ ∅, generate_open.basic _ ⟨{s}, ⟨finite_singleton s, singleton_subset_iff.2 hs,
-            by rwa [sInter_singleton]⟩, sInter_singleton s⟩))
-      (generate_from_le $ assume u ⟨t, ⟨hft, htb, ne⟩, eq⟩,
-        eq ▸ @is_open_sInter _ (generate_from s) _ hft (assume s hs, generate_open.basic _ $ htb hs)),
+            by rwa [sInter_singleton]⟩, sInter_singleton s⟩)),
   this ▸ hs⟩
 
 lemma is_topological_basis_of_open_of_nhds {s : set (set α)}
@@ -60,11 +60,11 @@ lemma is_topological_basis_of_open_of_nhds {s : set (set α)}
     let ⟨u, h₁, h₂, _⟩ := h_nhds a univ trivial (is_open_univ _) in
     ⟨u, h₁, h₂⟩,
   le_antisymm
+    (le_generate_from h_open)
     (assume u hu,
       (@is_open_iff_nhds α (generate_from _) _).mpr $ assume a hau,
         let ⟨v, hvs, hav, hvu⟩ := h_nhds a u hau hu in
-        by rw nhds_generate_from; exact infi_le_of_le v (infi_le_of_le ⟨hav, hvs⟩ $ le_principal_iff.2 hvu))
-    (generate_from_le h_open)⟩
+        by rw nhds_generate_from; exact infi_le_of_le v (infi_le_of_le ⟨hav, hvs⟩ $ le_principal_iff.2 hvu))⟩
 
 lemma mem_nhds_of_is_topological_basis {a : α} {s : set α} {b : set (set α)}
   (hb : is_topological_basis b) : s ∈ nhds a ↔ ∃t∈b, a ∈ t ∧ t ⊆ s :=