diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean index 67eb58978f762..f86cca6bfa443 100644 --- a/src/data/set/finite.lean +++ b/src/data/set/finite.lean @@ -1280,7 +1280,7 @@ 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 := @@ -1288,7 +1288,7 @@ 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 diff --git a/src/order/bounds/basic.lean b/src/order/bounds/basic.lean index 6cfd3c71db1d3..6add0bb14d555 100644 --- a/src/order/bounds/basic.lean +++ b/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 diff --git a/src/order/directed.lean b/src/order/directed.lean index 83c44b4bf2b62..0456ab1e72b13 100644 --- a/src/order/directed.lean +++ b/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 diff --git a/src/order/liminf_limsup.lean b/src/order/liminf_limsup.lean index adafe31cd2008..ececbb65f3515 100644 --- a/src/order/liminf_limsup.lean +++ b/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 diff --git a/src/topology/algebra/order/liminf_limsup.lean b/src/topology/algebra/order/liminf_limsup.lean index 4e819a7cdbfb6..c16bae4dda725 100644 --- a/src/topology/algebra/order/liminf_limsup.lean +++ b/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