chore(order/liminf_limsup): Generalise and move lemmas (#18628)

Generalise lemmas from semilattices to codirected orders. Move topology-less lemmas from `topology.algebra.order.liminf_limsup` to `order.liminf_limsup`. Also turn arguments to `bdd_above_insert` and friends implicit.

Author: YaelDillies

src/data/set/finite.lean

@@ -1280,15 +1280,15 @@ end
 
 section
 
-variables [semilattice_sup α] [nonempty α] {s : set α}
+variables [preorder α] [is_directed α (≤)] [nonempty α] {s : set α}
 
 /--A finite set is bounded above.-/
 protected lemma finite.bdd_above (hs : s.finite) : bdd_above s :=
 finite.induction_on hs bdd_above_empty $ λ a s _ _ h, h.insert a
 
 /--A finite union of sets which are all bounded above is still bounded above.-/
 lemma finite.bdd_above_bUnion {I : set β} {S : β → set α} (H : I.finite) :
-  (bdd_above (⋃i∈I, S i)) ↔ (∀i ∈ I, bdd_above (S i)) :=
+  bdd_above (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, bdd_above (S i) :=
 finite.induction_on H
   (by simp only [bUnion_empty, bdd_above_empty, ball_empty_iff])
   (λ a s ha _ hs, by simp only [bUnion_insert, ball_insert_iff, bdd_above_union, hs])
@@ -1299,22 +1299,17 @@ end
 
 section
 
-variables [semilattice_inf α] [nonempty α] {s : set α}
+variables [preorder α] [is_directed α (≥)] [nonempty α] {s : set α}
 
 /--A finite set is bounded below.-/
-protected lemma finite.bdd_below (hs : s.finite) : bdd_below s := @finite.bdd_above αᵒᵈ _ _ _ hs
+protected lemma finite.bdd_below (hs : s.finite) : bdd_below s := @finite.bdd_above αᵒᵈ _ _ _ _ hs
 
 /--A finite union of sets which are all bounded below is still bounded below.-/
 lemma finite.bdd_below_bUnion {I : set β} {S : β → set α} (H : I.finite) :
   bdd_below (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, bdd_below (S i) :=
-@finite.bdd_above_bUnion αᵒᵈ _ _ _ _ _ H
+@finite.bdd_above_bUnion αᵒᵈ _ _ _ _ _ _ H
 
-lemma infinite_of_not_bdd_below : ¬ bdd_below s → s.infinite :=
-begin
-  contrapose!,
-  rw not_infinite,
-  apply finite.bdd_below,
-end
+lemma infinite_of_not_bdd_below : ¬ bdd_below s → s.infinite := mt finite.bdd_below
 
 end
 

src/order/bounds/basic.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Yury Kudryashov
 -/
 import data.set.intervals.basic
 import data.set.n_ary
+import order.directed
 
 /-!
 
@@ -283,31 +284,30 @@ h.mono $ inter_subset_left s t
 lemma bdd_below.inter_of_right (h : bdd_below t) : bdd_below (s ∩ t) :=
 h.mono $ inter_subset_right s t
 
-/-- If `s` and `t` are bounded above sets in a `semilattice_sup`, then so is `s ∪ t`. -/
-lemma bdd_above.union [semilattice_sup γ] {s t : set γ} :
+/-- In a directed order, the union of bounded above sets is bounded above. -/
+lemma bdd_above.union [is_directed α (≤)] {s t : set α} :
   bdd_above s → bdd_above t → bdd_above (s ∪ t) :=
 begin
-  rintros ⟨bs, hs⟩ ⟨bt, ht⟩,
-  use bs ⊔ bt,
-  rw upper_bounds_union,
-  exact ⟨upper_bounds_mono_mem le_sup_left hs,
-    upper_bounds_mono_mem le_sup_right ht⟩
+  rintro ⟨a, ha⟩ ⟨b, hb⟩,
+  obtain ⟨c, hca, hcb⟩ := exists_ge_ge a b,
+  rw [bdd_above, upper_bounds_union],
+  exact ⟨c, upper_bounds_mono_mem hca ha, upper_bounds_mono_mem hcb hb⟩,
 end
 
-/-- The union of two sets is bounded above if and only if each of the sets is. -/
-lemma bdd_above_union [semilattice_sup γ] {s t : set γ} :
+/-- In a directed order, the union of two sets is bounded above if and only if both sets are. -/
+lemma bdd_above_union [is_directed α (≤)] {s t : set α} :
   bdd_above (s ∪ t) ↔ bdd_above s ∧ bdd_above t :=
-⟨λ h, ⟨h.mono $ subset_union_left s t, h.mono $ subset_union_right s t⟩,
-  λ h, h.1.union h.2⟩
+⟨λ h, ⟨h.mono $ subset_union_left _ _, h.mono $ subset_union_right _ _⟩, λ h, h.1.union h.2⟩
 
-lemma bdd_below.union [semilattice_inf γ] {s t : set γ} :
+/-- In a codirected order, the union of bounded below sets is bounded below. -/
+lemma bdd_below.union [is_directed α (≥)] {s t : set α} :
   bdd_below s → bdd_below t → bdd_below (s ∪ t) :=
-@bdd_above.union γᵒᵈ _ s t
+@bdd_above.union αᵒᵈ _ _ _ _
 
-/--The union of two sets is bounded above if and only if each of the sets is.-/
-lemma bdd_below_union [semilattice_inf γ] {s t : set γ} :
+/-- In a codirected order, the union of two sets is bounded below if and only if both sets are. -/
+lemma bdd_below_union [is_directed α (≥)] {s t : set α} :
   bdd_below (s ∪ t) ↔ bdd_below s ∧ bdd_below t :=
-@bdd_above_union γᵒᵈ _ s t
+@bdd_above_union αᵒᵈ _ _ _ _
 
 /-- If `a` is the least upper bound of `s` and `b` is the least upper bound of `t`,
 then `a ⊔ b` is the least upper bound of `s ∪ t`. -/
@@ -642,22 +642,22 @@ lemma nonempty_of_not_bdd_below [ha : nonempty α] (h : ¬bdd_below s) : s.nonem
 -/
 
 /-- Adding a point to a set preserves its boundedness above. -/
-@[simp] lemma bdd_above_insert [semilattice_sup γ] (a : γ) {s : set γ} :
+@[simp] lemma bdd_above_insert [is_directed α (≤)] {s : set α} {a : α} :
   bdd_above (insert a s) ↔ bdd_above s :=
 by simp only [insert_eq, bdd_above_union, bdd_above_singleton, true_and]
 
-lemma bdd_above.insert [semilattice_sup γ] (a : γ) {s : set γ} (hs : bdd_above s) :
-  bdd_above (insert a s) :=
-(bdd_above_insert a).2 hs
+protected lemma bdd_above.insert [is_directed α (≤)] {s : set α} (a : α) :
+  bdd_above s → bdd_above (insert a s) :=
+bdd_above_insert.2
 
 /--Adding a point to a set preserves its boundedness below.-/
-@[simp] lemma bdd_below_insert [semilattice_inf γ] (a : γ) {s : set γ} :
+@[simp] lemma bdd_below_insert [is_directed α (≥)] {s : set α} {a : α} :
   bdd_below (insert a s) ↔ bdd_below s :=
 by simp only [insert_eq, bdd_below_union, bdd_below_singleton, true_and]
 
-lemma bdd_below.insert [semilattice_inf γ] (a : γ) {s : set γ} (hs : bdd_below s) :
-  bdd_below (insert a s) :=
-(bdd_below_insert a).2 hs
+lemma bdd_below.insert [is_directed α (≥)] {s : set α} (a : α) :
+  bdd_below s → bdd_below (insert a s) :=
+bdd_below_insert.2
 
 lemma is_lub.insert [semilattice_sup γ] (a) {b} {s : set γ} (hs : is_lub s b) :
   is_lub (insert a s) (a ⊔ b) :=
@@ -1191,3 +1191,32 @@ end
 lemma is_glb_prod [preorder α] [preorder β] {s : set (α × β)} (p : α × β) :
   is_glb s p ↔ is_glb (prod.fst '' s) p.1 ∧ is_glb (prod.snd '' s) p.2 :=
 @is_lub_prod αᵒᵈ βᵒᵈ _ _ _ _
+
+section scott_continuous
+variables [preorder α] [preorder β] {f : α → β} {a : α}
+
+/-- A function between preorders is said to be Scott continuous if it preserves `is_lub` on directed
+sets. It can be shown that a function is Scott continuous if and only if it is continuous wrt the
+Scott topology.
+
+The dual notion
+
+```lean
+∀ ⦃d : set α⦄, d.nonempty → directed_on (≥) d → ∀ ⦃a⦄, is_glb d a → is_glb (f '' d) (f a)
+```
+
+does not appear to play a significant role in the literature, so is omitted here.
+-/
+def scott_continuous (f : α → β) : Prop :=
+∀ ⦃d : set α⦄, d.nonempty → directed_on (≤) d → ∀ ⦃a⦄, is_lub d a → is_lub (f '' d) (f a)
+
+protected lemma scott_continuous.monotone (h : scott_continuous f) : monotone f :=
+begin
+  refine λ a b hab, (h (insert_nonempty _ _) (directed_on_pair le_refl hab) _).1
+    (mem_image_of_mem _ $ mem_insert _ _),
+  rw [is_lub, upper_bounds_insert, upper_bounds_singleton,
+    inter_eq_self_of_subset_right (Ici_subset_Ici.2 hab)],
+  exact is_least_Ici,
+end
+
+end scott_continuous

src/order/directed.lean

@@ -6,7 +6,6 @@ Authors: Johannes Hölzl
 import data.set.image
 import order.lattice
 import order.max
-import order.bounds.basic
 
 /-!
 # Directed indexed families and sets
@@ -259,42 +258,3 @@ instance order_top.to_is_directed_le [has_le α] [order_top α] : is_directed α
 @[priority 100]  -- see Note [lower instance priority]
 instance order_bot.to_is_directed_ge [has_le α] [order_bot α] : is_directed α (≥) :=
 ⟨λ a b, ⟨⊥, bot_le, bot_le⟩⟩
-
-section scott_continuous
-
-variables [preorder α] {a : α}
-
-/--
-A function between preorders is said to be Scott continuous if it preserves `is_lub` on directed
-sets. It can be shown that a function is Scott continuous if and only if it is continuous wrt the
-Scott topology.
-
-The dual notion
-
-```lean
-∀ ⦃d : set α⦄, d.nonempty → directed_on (≥) d → ∀ ⦃a⦄, is_glb d a → is_glb (f '' d) (f a)
-```
-
-does not appear to play a significant role in the literature, so is omitted here.
--/
-def scott_continuous [preorder β] (f : α → β) : Prop :=
-∀ ⦃d : set α⦄, d.nonempty → directed_on (≤) d → ∀ ⦃a⦄, is_lub d a → is_lub (f '' d) (f a)
-
-protected lemma scott_continuous.monotone [preorder β] {f : α → β}
-  (h : scott_continuous f) :
-  monotone f :=
-begin
-  intros a b hab,
-  have e1 : is_lub (f '' {a, b}) (f b),
-  { apply h,
-    { exact set.insert_nonempty _ _ },
-    { exact directed_on_pair le_refl hab },
-    { rw [is_lub, upper_bounds_insert, upper_bounds_singleton,
-        set.inter_eq_self_of_subset_right (set.Ici_subset_Ici.mpr hab)],
-      exact is_least_Ici } },
-  apply e1.1,
-  rw set.image_pair,
-  exact set.mem_insert _ _,
-end
-
-end scott_continuous

src/order/liminf_limsup.lean

@@ -122,7 +122,7 @@ lemma not_is_bounded_under_of_tendsto_at_bot [preorder β] [no_min_order β] {f
   ¬ is_bounded_under (≥) l f :=
 @not_is_bounded_under_of_tendsto_at_top α βᵒᵈ _ _ _ _ _ hf
 
-lemma is_bounded_under.bdd_above_range_of_cofinite [semilattice_sup β] {f : α → β}
+lemma is_bounded_under.bdd_above_range_of_cofinite [preorder β] [is_directed β (≤)] {f : α → β}
   (hf : is_bounded_under (≤) cofinite f) : bdd_above (range f) :=
 begin
   rcases hf with ⟨b, hb⟩,
@@ -131,17 +131,17 @@ begin
   exact ⟨⟨b, ball_image_iff.2 $ λ x, id⟩, (hb.image f).bdd_above⟩
 end
 
-lemma is_bounded_under.bdd_below_range_of_cofinite [semilattice_inf β] {f : α → β}
+lemma is_bounded_under.bdd_below_range_of_cofinite [preorder β] [is_directed β (≥)] {f : α → β}
   (hf : is_bounded_under (≥) cofinite f) : bdd_below (range f) :=
-@is_bounded_under.bdd_above_range_of_cofinite α βᵒᵈ _ _ hf
+@is_bounded_under.bdd_above_range_of_cofinite α βᵒᵈ _ _ _ hf
 
-lemma is_bounded_under.bdd_above_range [semilattice_sup β] {f : ℕ → β}
+lemma is_bounded_under.bdd_above_range [preorder β] [is_directed β (≤)] {f : ℕ → β}
   (hf : is_bounded_under (≤) at_top f) : bdd_above (range f) :=
 by { rw ← nat.cofinite_eq_at_top at hf, exact hf.bdd_above_range_of_cofinite }
 
-lemma is_bounded_under.bdd_below_range [semilattice_inf β] {f : ℕ → β}
+lemma is_bounded_under.bdd_below_range [preorder β] [is_directed β (≥)] {f : ℕ → β}
   (hf : is_bounded_under (≥) at_top f) : bdd_below (range f) :=
-@is_bounded_under.bdd_above_range βᵒᵈ _ _ hf
+@is_bounded_under.bdd_above_range βᵒᵈ _ _ _ hf
 
 /-- `is_cobounded (≺) f` states that the filter `f` does not tend to infinity w.r.t. `≺`. This is
 also called frequently bounded. Will be usually instantiated with `≤` or `≥`.
@@ -198,6 +198,31 @@ lemma is_cobounded.mono (h : f ≤ g) : f.is_cobounded r → g.is_cobounded r
 
 end relation
 
+section nonempty
+variables [preorder α] [nonempty α] {f : filter β} {u : β → α}
+
+lemma is_bounded_le_at_bot : (at_bot : filter α).is_bounded (≤) :=
+‹nonempty α›.elim $ λ a, ⟨a, eventually_le_at_bot _⟩
+
+lemma is_bounded_ge_at_top : (at_top : filter α).is_bounded (≥) :=
+‹nonempty α›.elim $ λ a, ⟨a, eventually_ge_at_top _⟩
+
+lemma tendsto.is_bounded_under_le_at_bot (h : tendsto u f at_bot) : f.is_bounded_under (≤) u :=
+is_bounded_le_at_bot.mono h
+
+lemma tendsto.is_bounded_under_ge_at_top (h : tendsto u f at_top) : f.is_bounded_under (≥) u :=
+is_bounded_ge_at_top.mono h
+
+lemma bdd_above_range_of_tendsto_at_top_at_bot [is_directed α (≤)] {u : ℕ → α}
+  (hx : tendsto u at_top at_bot) : bdd_above (set.range u) :=
+hx.is_bounded_under_le_at_bot.bdd_above_range
+
+lemma bdd_below_range_of_tendsto_at_top_at_top [is_directed α (≥)] {u : ℕ → α}
+  (hx : tendsto u at_top at_top) : bdd_below (set.range u) :=
+hx.is_bounded_under_ge_at_top.bdd_below_range
+
+end nonempty
+
 lemma is_cobounded_le_of_bot [preorder α] [order_bot α] {f : filter α} : f.is_cobounded (≤) :=
 ⟨⊥, assume a h, bot_le⟩
 
@@ -955,6 +980,15 @@ lemma frequently_lt_of_liminf_lt {α β} [conditionally_complete_linear_order β
   ∃ᶠ x in f, u x < b :=
 @frequently_lt_of_lt_limsup _ βᵒᵈ _ f u b hu h
 
+variables [conditionally_complete_linear_order α] {f : filter α} {b : α}
+
+lemma lt_mem_sets_of_Limsup_lt (h : f.is_bounded (≤)) (l : f.Limsup < b) : ∀ᶠ a in f, a < b :=
+let ⟨c, (h : ∀ᶠ a in f, a ≤ c), hcb⟩ := exists_lt_of_cInf_lt h l in
+mem_of_superset h $ λ a, hcb.trans_le'
+
+lemma gt_mem_sets_of_Liminf_gt : f.is_bounded (≥) → b < f.Liminf → ∀ᶠ a in f, b < a :=
+@lt_mem_sets_of_Limsup_lt αᵒᵈ _ _ _
+
 end conditionally_complete_linear_order
 
 end filter

src/topology/algebra/order/liminf_limsup.lean

@@ -51,19 +51,6 @@ lemma filter.tendsto.is_cobounded_under_ge {f : filter β} {u : β → α} {a :
   [ne_bot f] (h : tendsto u f (𝓝 a)) : f.is_cobounded_under (≥) u :=
 h.is_bounded_under_le.is_cobounded_flip
 
-lemma is_bounded_le_at_bot (α : Type*) [hα : nonempty α] [preorder α] :
-  (at_bot : filter α).is_bounded (≤) :=
-is_bounded_iff.2 ⟨set.Iic hα.some, mem_at_bot _, hα.some, λ x hx, hx⟩
-
-lemma filter.tendsto.is_bounded_under_le_at_bot {α : Type*} [nonempty α] [preorder α]
-  {f : filter β} {u : β → α} (h : tendsto u f at_bot) :
-  f.is_bounded_under (≤) u :=
-(is_bounded_le_at_bot α).mono h
-
-lemma bdd_above_range_of_tendsto_at_top_at_bot {α : Type*} [nonempty α] [semilattice_sup α]
-  {u : ℕ → α} (hx : tendsto u at_top at_bot) : bdd_above (set.range u) :=
-(filter.tendsto.is_bounded_under_le_at_bot hx).bdd_above_range
-
 end order_closed_topology
 
 section order_closed_topology
@@ -90,33 +77,11 @@ lemma filter.tendsto.is_cobounded_under_le {f : filter β} {u : β → α} {a :
   [ne_bot f] (h : tendsto u f (𝓝 a)) : f.is_cobounded_under (≤) u :=
 h.is_bounded_under_ge.is_cobounded_flip
 
-lemma is_bounded_ge_at_top (α : Type*) [hα : nonempty α] [preorder α] :
-  (at_top : filter α).is_bounded (≥) :=
-is_bounded_le_at_bot αᵒᵈ
-
-lemma filter.tendsto.is_bounded_under_ge_at_top {α : Type*} [nonempty α] [preorder α]
-  {f : filter β} {u : β → α} (h : tendsto u f at_top) :
-  f.is_bounded_under (≥) u :=
-(is_bounded_ge_at_top α).mono h
-
-lemma bdd_below_range_of_tendsto_at_top_at_top {α : Type*} [nonempty α] [semilattice_inf α]
-  {u : ℕ → α} (hx : tendsto u at_top at_top) : bdd_below (set.range u) :=
-(filter.tendsto.is_bounded_under_ge_at_top hx).bdd_below_range
-
 end order_closed_topology
 
 section conditionally_complete_linear_order
 variables [conditionally_complete_linear_order α]
 
-theorem lt_mem_sets_of_Limsup_lt {f : filter α} {b} (h : f.is_bounded (≤)) (l : f.Limsup < b) :
-  ∀ᶠ a in f, a < b :=
-let ⟨c, (h : ∀ᶠ a in f, a ≤ c), hcb⟩ := exists_lt_of_cInf_lt h l in
-mem_of_superset h $ assume a hac, lt_of_le_of_lt hac hcb
-
-theorem gt_mem_sets_of_Liminf_gt : ∀ {f : filter α} {b}, f.is_bounded (≥) → b < f.Liminf →
-  ∀ᶠ a in f, b < a :=
-@lt_mem_sets_of_Limsup_lt αᵒᵈ _
-
 variables [topological_space α] [order_topology α]
 
 /-- If the liminf and the limsup of a filter coincide, then this filter converges to