feat(topology/algebra/ordered): add order topology for partial orders… (#1276)

* feat(topology/algebra/ordered): doc, add convergence in ordered groups criterion

* docstring

* reviewer's comments

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: 3 people

scripts/nolints.txt

@@ -1340,7 +1340,7 @@ ideal.quotient_inf_to_pi_quotient
 ideal.radical
 ideal.radical_pow
 ideal.span
-induced_orderable_topology'
+induced_order_topology'
 inducing
 infi_eq_elim
 infi_real_pos_eq_infi_nnreal_pos
@@ -1718,7 +1718,7 @@ measure_theory.simple_func.range
 measure_theory.simple_func.restrict
 measure_theory.simple_func.seq
 measure_theory.volume
-mem_nhds_orderable_dest
+mem_nhds_order_dest
 mem_uniformity_edist
 metric.Hausdorff_dist_le_of_inf_dist
 metric.cauchy_iff
@@ -1869,7 +1869,7 @@ nat.totient
 nat.unpaired
 nat.xgcd_aux
 nhds_contain_boxes
-nhds_eq_orderable
+nhds_eq_order
 nnreal.le_of_forall_epsilon_le
 nnreal.le_of_real_iff_coe_le
 nnreal.of_real
@@ -2212,7 +2212,7 @@ order_iso.symm
 order_iso.to_order_embedding
 order_iso.trans
 order_of_pos
-orderable_topology_of_nhds_abs
+order_topology_of_nhds_abs
 ordering.compares.eq_gt
 ordinal.CNF_rec
 ordinal.CNF_sorted
@@ -3176,7 +3176,7 @@ tactic.unprime
 tactic.using_texpr
 tactic.valid_types
 tactic.wlog
-tendsto_orderable
+tendsto_order
 tensor_product
 tensor_product.assoc
 tensor_product.comm

src/analysis/calculus/mean_value.lean

@@ -89,7 +89,7 @@ begin
   have A : continuous_on (λ x, (f x, B x)) (Icc a b), from hf.prod hB,
   have : is_closed s,
   { simp only [s, inter_comm],
-    exact A.preimage_closed_of_closed is_closed_Icc (ordered_topology.is_closed_le' _) },
+    exact A.preimage_closed_of_closed is_closed_Icc (order_closed_topology.is_closed_le' _) },
   apply this.Icc_subset_of_forall_exists_gt ha,
   rintros x ⟨hxB, xab⟩ y hy,
   change f x ≤ B x at hxB,

src/analysis/specific_limits.lean

@@ -86,7 +86,7 @@ tendsto_at_top_mul_right' (inv_pos hr) hf
 
 /-- The function `x ↦ x⁻¹` tends to `+∞` on the right of `0`. -/
 lemma tendsto_inv_zero_at_top [discrete_linear_ordered_field α] [topological_space α]
-  [orderable_topology α] : tendsto (λx:α, x⁻¹) (nhds_within (0 : α) (set.Ioi 0)) at_top :=
+  [order_topology α] : tendsto (λx:α, x⁻¹) (nhds_within (0 : α) (set.Ioi 0)) at_top :=
 begin
   apply (tendsto_at_top _ _).2 (λb, _),
   refine mem_nhds_within_Ioi_iff_exists_Ioo_subset.2 ⟨(max b 1)⁻¹, by simp [zero_lt_one], λx hx, _⟩,
@@ -99,7 +99,7 @@ end
 
 /-- The function `r ↦ r⁻¹` tends to `0` on the right as `r → +∞`. -/
 lemma tendsto_inv_at_top_zero' [discrete_linear_ordered_field α] [topological_space α]
-  [orderable_topology α] : tendsto (λr:α, r⁻¹) at_top (nhds_within (0 : α) (set.Ioi 0)) :=
+  [order_topology α] : tendsto (λr:α, r⁻¹) at_top (nhds_within (0 : α) (set.Ioi 0)) :=
 begin
   assume s hs,
   rw mem_nhds_within_Ioi_iff_exists_Ioc_subset at hs,
@@ -111,7 +111,7 @@ begin
 end
 
 lemma tendsto_inv_at_top_zero [discrete_linear_ordered_field α] [topological_space α]
-  [orderable_topology α] : tendsto (λr:α, r⁻¹) at_top (𝓝 0) :=
+  [order_topology α] : tendsto (λr:α, r⁻¹) at_top (𝓝 0) :=
 tendsto_le_right inf_le_left tendsto_inv_at_top_zero'
 
 lemma summable_of_absolute_convergence_real {f : ℕ → ℝ} :

src/measure_theory/ae_eq_fun.lean

@@ -541,7 +541,7 @@ end normed_space
 
 section pos_part
 
-variables {γ : Type*} [topological_space γ] [decidable_linear_order γ] [ordered_topology γ]
+variables {γ : Type*} [topological_space γ] [decidable_linear_order γ] [order_closed_topology γ]
   [second_countable_topology γ] [has_zero γ]
 
 /-- Positive part of an `ae_eq_fun`. -/

src/measure_theory/borel_space.lean

@@ -53,11 +53,11 @@ le_antisymm
 
 lemma borel_eq_generate_Iio (α)
   [topological_space α] [second_countable_topology α]
-  [linear_order α] [orderable_topology α] :
+  [linear_order α] [order_topology α] :
   borel α = generate_from (range Iio) :=
 begin
   refine le_antisymm _ (generate_from_le _),
-  { rw borel_eq_generate_from_of_subbasis (orderable_topology.topology_eq_generate_intervals α),
+  { rw borel_eq_generate_from_of_subbasis (order_topology.topology_eq_generate_intervals α),
     have H : ∀ a:α, is_measurable (measurable_space.generate_from (range Iio)) (Iio a) :=
       λ a, generate_measurable.basic _ ⟨_, rfl⟩,
     refine generate_from_le _, rintro _ ⟨a, rfl | rfl⟩; [skip, apply H],
@@ -86,11 +86,11 @@ end
 
 lemma borel_eq_generate_Ioi (α)
   [topological_space α] [second_countable_topology α]
-  [linear_order α] [orderable_topology α] :
+  [linear_order α] [order_topology α] :
   borel α = generate_from (range (λ a, {x | a < x})) :=
 begin
   refine le_antisymm _ (generate_from_le _),
-  { rw borel_eq_generate_from_of_subbasis (orderable_topology.topology_eq_generate_intervals α),
+  { rw borel_eq_generate_from_of_subbasis (order_topology.topology_eq_generate_intervals α),
     have H : ∀ a:α, is_measurable (measurable_space.generate_from (range (λ a, {x | a < x}))) {x | a < x} :=
       λ a, generate_measurable.basic _ ⟨_, rfl⟩,
     refine generate_from_le _, rintro _ ⟨a, rfl | rfl⟩, {apply H},
@@ -232,25 +232,25 @@ lemma measurable.mul
 measurable_of_continuous2 continuous_mul
 
 lemma is_measurable_le {α β}
-  [topological_space α] [partial_order α] [ordered_topology α] [second_countable_topology α]
+  [topological_space α] [partial_order α] [order_closed_topology α] [second_countable_topology α]
   [measurable_space β] {f : β → α} {g : β → α} (hf : measurable f) (hg : measurable g) :
   is_measurable {a | f a ≤ g a} :=
 have is_measurable {p : α × α | p.1 ≤ p.2},
-  by rw borel_prod; exact is_measurable_of_is_closed (ordered_topology.is_closed_le' _),
+  by rw borel_prod; exact is_measurable_of_is_closed (order_closed_topology.is_closed_le' _),
 show is_measurable {a | (f a, g a).1 ≤ (f a, g a).2},
 begin
   refine measurable.preimage _ this,
   exact measurable.prod_mk hf hg
 end
 
 lemma measurable.max {α β}
-  [topological_space α] [decidable_linear_order α] [ordered_topology α] [second_countable_topology α]
+  [topological_space α] [decidable_linear_order α] [order_closed_topology α] [second_countable_topology α]
   [measurable_space β] {f : β → α} {g : β → α} (hf : measurable f) (hg : measurable g) :
   measurable (λa, max (f a) (g a)) :=
 measurable.if (is_measurable_le hf hg) hg hf
 
 lemma measurable.min {α β}
-  [topological_space α] [decidable_linear_order α] [ordered_topology α] [second_countable_topology α]
+  [topological_space α] [decidable_linear_order α] [order_closed_topology α] [second_countable_topology α]
   [measurable_space β] {f : β → α} {g : β → α} (hf : measurable f) (hg : measurable g) :
   measurable (λa, min (f a) (g a)) :=
 measurable.if (is_measurable_le hf hg) hf hg
@@ -259,8 +259,8 @@ measurable.if (is_measurable_le hf hg) hf hg
 lemma measurable_coe_int_real : measurable (λa, a : ℤ → ℝ) :=
 assume s (hs : is_measurable s), by trivial
 
-section ordered_topology
-variables [linear_order α] [ordered_topology α] {a b c : α}
+section order_closed_topology
+variables [linear_order α] [order_closed_topology α] {a b c : α}
 
 lemma is_measurable_Ioo : is_measurable (Ioo a b) := is_measurable_of_is_open is_open_Ioo
 
@@ -270,10 +270,10 @@ lemma is_measurable_Ico : is_measurable (Ico a b) :=
 (is_measurable_of_is_closed $ is_closed_le continuous_const continuous_id).inter
   is_measurable_Iio
 
-end ordered_topology
+end order_closed_topology
 
 lemma measurable.is_lub {α} [topological_space α] [linear_order α]
-  [orderable_topology α] [second_countable_topology α]
+  [order_topology α] [second_countable_topology α]
   {β} [measurable_space β] {ι} [encodable ι]
   {f : ι → β → α} {g : β → α} (hf : ∀ i, measurable (f i))
   (hg : ∀ b, is_lub {a | ∃ i, f i b = a} (g b)) :
@@ -291,7 +291,7 @@ begin
 end
 
 lemma measurable.is_glb {α} [topological_space α] [linear_order α]
-  [orderable_topology α] [second_countable_topology α]
+  [order_topology α] [second_countable_topology α]
   {β} [measurable_space β] {ι} [encodable ι]
   {f : ι → β → α} {g : β → α} (hf : ∀ i, measurable (f i))
   (hg : ∀ b, is_glb {a | ∃ i, f i b = a} (g b)) :
@@ -309,14 +309,14 @@ begin
 end
 
 lemma measurable.supr {α} [topological_space α] [complete_linear_order α]
-  [orderable_topology α] [second_countable_topology α]
+  [order_topology α] [second_countable_topology α]
   {β} [measurable_space β] {ι} [encodable ι]
   {f : ι → β → α} (hf : ∀ i, measurable (f i)) :
   measurable (λ b, ⨆ i, f i b) :=
 measurable.is_lub hf $ λ b, is_lub_supr
 
 lemma measurable.infi {α} [topological_space α] [complete_linear_order α]
-  [orderable_topology α] [second_countable_topology α]
+  [order_topology α] [second_countable_topology α]
   {β} [measurable_space β] {ι} [encodable ι]
   {f : ι → β → α} (hf : ∀ i, measurable (f i)) :
   measurable (λ b, ⨅ i, f i b) :=

src/measure_theory/integration.lean

@@ -303,7 +303,7 @@ of the set `{i k | k ≤ n ∧ i k ≤ f a}`, see `approx_apply` and `supr_appro
 def approx (i : ℕ → β) (f : α → β) (n : ℕ) : α →ₛ β :=
 (finset.range n).sup (λk, restrict (const α (i k)) {a:α | i k ≤ f a})
 
-lemma approx_apply [topological_space β] [ordered_topology β] {i : ℕ → β} {f : α → β} {n : ℕ}
+lemma approx_apply [topological_space β] [order_closed_topology β] {i : ℕ → β} {f : α → β} {n : ℕ}
   (a : α) (hf : _root_.measurable f) :
   (approx i f n : α →ₛ β) a = (finset.range n).sup (λk, if i k ≤ f a then i k else 0) :=
 begin
@@ -319,15 +319,15 @@ end
 lemma monotone_approx (i : ℕ → β) (f : α → β) : monotone (approx i f) :=
 assume n m h, finset.sup_mono $ finset.range_subset.2 h
 
-lemma approx_comp [topological_space β] [ordered_topology β] [measurable_space γ]
+lemma approx_comp [topological_space β] [order_closed_topology β] [measurable_space γ]
   {i : ℕ → β} {f : γ → β} {g : α → γ} {n : ℕ} (a : α)
   (hf : _root_.measurable f) (hg : _root_.measurable g) :
   (approx i (f ∘ g) n : α →ₛ β) a = (approx i f n : γ →ₛ β) (g a) :=
 by rw [approx_apply _ hf, approx_apply _ (hf.comp hg)]
 
 end
 
-lemma supr_approx_apply [topological_space β] [complete_lattice β] [ordered_topology β] [has_zero β]
+lemma supr_approx_apply [topological_space β] [complete_lattice β] [order_closed_topology β] [has_zero β]
   (i : ℕ → β) (f : α → β) (a : α) (hf : _root_.measurable f) (h_zero : (0 : β) = ⊥) :
   (⨆n, (approx i f n : α →ₛ β) a) = (⨆k (h : i k ≤ f a), i k) :=
 begin

src/tactic/lint.lean

@@ -246,6 +246,12 @@ return $ let illegal := [`gt, `ge] in if d.type.contains_constant (λ n, n ∈ i
   errors_found := "ILLEGAL CONSTANTS IN DECLARATIONS",
   is_fast := ff }
 
+library_note "nolint_ge" "Currently, the linter forbids the use of `>` and `≥` in definitions and
+statements, as they cause problems in rewrites. However, we still allow them in some contexts,
+for instance when expressing properties of the operator (as in `cobounded (≥)`), or in quantifiers
+such as `∀ ε > 0`. Such statements should be marked with the attribute `nolint` to avoid linter
+failures."
+
 /-- checks whether an instance that always applies has priority ≥ 1000. -/
 -- TODO: instance_priority should also be tested on automatically-generated declarations
 meta def instance_priority (d : declaration) : tactic (option string) := do

src/topology/algebra/infinite_sum.lean

@@ -453,7 +453,7 @@ end tsum
 end topological_semiring
 
 section order_topology
-variables [ordered_comm_monoid α] [topological_space α] [ordered_topology α]
+variables [ordered_comm_monoid α] [topological_space α] [order_closed_topology α]
 variables {f g : β → α} {a a₁ a₂ : α}
 
 lemma has_sum_le (h : ∀b, f b ≤ g b) (hf : has_sum f a₁) (hg : has_sum g a₂) : a₁ ≤ a₂ :=