diff --git a/Mathlib.lean b/Mathlib.lean index 7c06adf341a5a..c0b37d8a3723e 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -990,6 +990,7 @@ import Mathlib.Topology.Maps import Mathlib.Topology.NhdsSet import Mathlib.Topology.OmegaCompletePartialOrder import Mathlib.Topology.Order +import Mathlib.Topology.Order.Basic import Mathlib.Topology.Paracompact import Mathlib.Topology.Separation import Mathlib.Topology.SubsetProperties diff --git a/Mathlib/Data/Set/Countable.lean b/Mathlib/Data/Set/Countable.lean index 85ef308db372e..2ade8317ab0b3 100644 --- a/Mathlib/Data/Set/Countable.lean +++ b/Mathlib/Data/Set/Countable.lean @@ -221,6 +221,9 @@ theorem Countable.union {s t : Set α} (hs : s.Countable) (ht : t.Countable) : ( countable_union.2 ⟨hs, ht⟩ #align set.countable.union Set.Countable.union +theorem Countable.of_diff {s t : Set α} (h : (s \ t).Countable) (ht : t.Countable) : s.Countable := + (h.union ht).mono (subset_diff_union _ _) + @[simp] theorem countable_insert {s : Set α} {a : α} : (insert a s).Countable ↔ s.Countable := by simp only [insert_eq, countable_union, countable_singleton, true_and_iff] diff --git a/Mathlib/Order/Cover.lean b/Mathlib/Order/Cover.lean index 10a1f4a262ae0..6a8c6b932ed6d 100644 --- a/Mathlib/Order/Cover.lean +++ b/Mathlib/Order/Cover.lean @@ -457,6 +457,15 @@ theorem Covby.eq_of_between {x : α} (hab : a ⋖ b) (hbc : b ⋖ c) (hax : a < le_antisymm (le_of_not_lt fun h => hbc.2 h hxc) (le_of_not_lt <| hab.2 hax) #align covby.eq_of_between Covby.eq_of_between +/-- If `a < b` then there exist `a' > a` and `b' < b` such that `Set.Iio a'` is strictly to the left +of `Set.Ioi b'`. -/ +lemma LT.lt.exists_disjoint_Iio_Ioi (h : a < b) : + ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y := by + by_cases h' : a ⋖ b + · exact ⟨b, h, a, h, fun x hx y hy => hx.trans_le <| h'.ge_of_gt hy⟩ + · rcases h.exists_lt_lt h' with ⟨c, ha, hb⟩ + exact ⟨c, ha, c, hb, fun _ h₁ _ => lt_trans h₁⟩ + end LinearOrder namespace Set diff --git a/Mathlib/Topology/ContinuousOn.lean b/Mathlib/Topology/ContinuousOn.lean index a4faa9dd3ba91..df88cb5693201 100644 --- a/Mathlib/Topology/ContinuousOn.lean +++ b/Mathlib/Topology/ContinuousOn.lean @@ -119,12 +119,8 @@ theorem nhds_of_nhdsWithin_of_nhds {s t : Set α} {a : α} (h1 : s ∈ 𝓝 a) ( #align nhds_of_nhds_within_of_nhds nhds_of_nhdsWithin_of_nhds theorem mem_nhdsWithin_iff_eventually {s t : Set α} {x : α} : - t ∈ 𝓝[s] x ↔ ∀ᶠ y in 𝓝 x, y ∈ s → y ∈ t := by - rw [mem_nhdsWithin_iff_exists_mem_nhds_inter] - constructor - · rintro ⟨u, hu, hut⟩ - exact eventually_of_mem hu fun x hxu hxs => hut ⟨hxu, hxs⟩ - · refine' fun h => ⟨_, h, fun y hy => hy.1 hy.2⟩ + t ∈ 𝓝[s] x ↔ ∀ᶠ y in 𝓝 x, y ∈ s → y ∈ t := + eventually_inf_principal #align mem_nhds_within_iff_eventually mem_nhdsWithin_iff_eventually theorem mem_nhdsWithin_iff_eventuallyEq {s t : Set α} {x : α} : @@ -271,6 +267,10 @@ theorem nhdsWithin_inter_of_mem {a : α} {s t : Set α} (h : s ∈ 𝓝[t] a) : exact nhdsWithin_le_of_mem h #align nhds_within_inter_of_mem nhdsWithin_inter_of_mem +-- porting note: new lemma +theorem nhdsWithin_inter_of_mem' {a : α} {s t : Set α} (h : t ∈ 𝓝[s] a) : 𝓝[s ∩ t] a = 𝓝[s] a := by + rw [inter_comm, nhdsWithin_inter_of_mem h] + @[simp] theorem nhdsWithin_singleton (a : α) : 𝓝[{a}] a = pure a := by rw [nhdsWithin, principal_singleton, inf_eq_right.2 (pure_le_nhds a)] diff --git a/Mathlib/Topology/Order/Basic.lean b/Mathlib/Topology/Order/Basic.lean new file mode 100644 index 0000000000000..2aacac080c2c8 --- /dev/null +++ b/Mathlib/Topology/Order/Basic.lean @@ -0,0 +1,2795 @@ +/- +Copyright (c) 2017 Johannes Hölzl. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov + +! This file was ported from Lean 3 source module topology.order.basic +! leanprover-community/mathlib commit b363547b3113d350d053abdf2884e9850a56b205 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.Data.Set.Intervals.Pi +import Mathlib.Data.Set.Pointwise.Interval +import Mathlib.Order.Filter.Interval +import Mathlib.Topology.Support +import Mathlib.Topology.Algebra.Order.LeftRight + +/-! +# Theory of topology on ordered spaces + +## Main definitions + +The order topology on an ordered space is the topology generated by all open intervals (or +equivalently by those of the form `(-∞, a)` and `(b, +∞)`). We define it as `Preorder.topology α`. +However, we do *not* register it as an instance (as many existing ordered types already have +topologies, which would be equal but not definitionally equal to `Preorder.topology α`). Instead, +we introduce a class `OrderTopology α` (which is a `Prop`, also known as a mixin) saying that on +the type `α` having already a topological space structure and a preorder structure, the topological +structure is equal to the order topology. + +We also introduce another (mixin) class `OrderClosedTopology α` saying that the set of points +`(x, y)` with `x ≤ y` is closed in the product space. This is automatically satisfied on a linear +order with the order topology. + +We prove many basic properties of such topologies. + +## Main statements + +This file contains the proofs of the following facts. For exact requirements +(`OrderClosedTopology` vs `OrderTopology`, `Preorder` vs `PartialOrder` vs `LinearOrder` etc) +see their statements. + +### Open / closed sets + +* `isOpen_lt` : if `f` and `g` are continuous functions, then `{x | f x < g x}` is open; +* `isOpen_Iio`, `isOpen_Ioi`, `isOpen_Ioo` : open intervals are open; +* `isClosed_le` : if `f` and `g` are continuous functions, then `{x | f x ≤ g x}` is closed; +* `isClosed_Iic`, `isClosed_Ici`, `isClosed_Icc` : closed intervals are closed; +* `frontier_le_subset_eq`, `frontier_lt_subset_eq` : frontiers of both `{x | f x ≤ g x}` + and `{x | f x < g x}` are included by `{x | f x = g x}`; +* `exists_Ioc_subset_of_mem_nhds`, `exists_Ico_subset_of_mem_nhds` : if `x < y`, then any + neighborhood of `x` includes an interval `[x, z)` for some `z ∈ (x, y]`, and any neighborhood + of `y` includes an interval `(z, y]` for some `z ∈ [x, y)`. + +### Convergence and inequalities + +* `le_of_tendsto_of_tendsto` : if `f` converges to `a`, `g` converges to `b`, and eventually + `f x ≤ g x`, then `a ≤ b` +* `le_of_tendsto`, `ge_of_tendsto` : if `f` converges to `a` and eventually `f x ≤ b` + (resp., `b ≤ f x`), then `a ≤ b` (resp., `b ≤ a); we also provide primed versions + that assume the inequalities to hold for all `x`. + +### Min, max, `Sup` and `Inf` + +* `Continuous.min`, `Continuous.max`: pointwise `min`/`max` of two continuous functions is + continuous. +* `Tendsto.min`, `Tendsto.max` : if `f` tends to `a` and `g` tends to `b`, then their pointwise + `min`/`max` tend to `min a b` and `max a b`, respectively. +* `tendsto_of_tendsto_of_tendsto_of_le_of_le` : theorem known as squeeze theorem, + sandwich theorem, theorem of Carabinieri, and two policemen (and a drunk) theorem; if `g` and `h` + both converge to `a`, and eventually `g x ≤ f x ≤ h x`, then `f` converges to `a`. + +## Implementation notes + +We do _not_ register the order topology as an instance on a preorder (or even on a linear order). +Indeed, on many such spaces, a topology has already been constructed in a different way (think +of the discrete spaces `ℕ` or `ℤ`, or `ℝ` that could inherit a topology as the completion of `ℚ`), +and is in general not defeq to the one generated by the intervals. We make it available as a +definition `preorder.topology α` though, that can be registered as an instance when necessary, or +for specific types. +-/ + + +open Set Filter TopologicalSpace Topology Function + +open OrderDual (toDual ofDual) + +universe u v w + +variable {α : Type u} {β : Type v} {γ : Type w} + +/-- A topology on a set which is both a topological space and a preorder is _order-closed_ if the +set of points `(x, y)` with `x ≤ y` is closed in the product space. We introduce this as a mixin. +This property is satisfied for the order topology on a linear order, but it can be satisfied more +generally, and suffices to derive many interesting properties relating order and topology. -/ +class OrderClosedTopology (α : Type _) [TopologicalSpace α] [Preorder α] : Prop where + /-- The set `{ (x, y) | x ≤ y }` is a closed set. -/ + isClosed_le' : IsClosed { p : α × α | p.1 ≤ p.2 } +#align order_closed_topology OrderClosedTopology + +instance [TopologicalSpace α] [h : FirstCountableTopology α] : FirstCountableTopology αᵒᵈ := h +instance [TopologicalSpace α] [h : SecondCountableTopology α] : SecondCountableTopology αᵒᵈ := h + +theorem Dense.orderDual [TopologicalSpace α] {s : Set α} (hs : Dense s) : + Dense (OrderDual.ofDual ⁻¹' s) := + hs +#align dense.order_dual Dense.orderDual + +section OrderClosedTopology + +section Preorder + +variable [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] + +namespace Subtype + +-- todo: add `OrderEmbedding.orderClosedtopology` +instance {p : α → Prop} : OrderClosedTopology (Subtype p) := + have this : Continuous fun p : Subtype p × Subtype p => ((p.fst : α), (p.snd : α)) := + continuous_subtype_val.prod_map continuous_subtype_val + OrderClosedTopology.mk (t.isClosed_le'.preimage this) + +end Subtype + +theorem isClosed_le_prod : IsClosed { p : α × α | p.1 ≤ p.2 } := + t.isClosed_le' +#align is_closed_le_prod isClosed_le_prod + +theorem isClosed_le [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) : + IsClosed { b | f b ≤ g b } := + continuous_iff_isClosed.mp (hf.prod_mk hg) _ isClosed_le_prod +#align is_closed_le isClosed_le + +theorem isClosed_le' (a : α) : IsClosed { b | b ≤ a } := + isClosed_le continuous_id continuous_const +#align is_closed_le' isClosed_le' + +theorem isClosed_Iic {a : α} : IsClosed (Iic a) := + isClosed_le' a +#align is_closed_Iic isClosed_Iic + +theorem isClosed_ge' (a : α) : IsClosed { b | a ≤ b } := + isClosed_le continuous_const continuous_id +#align is_closed_ge' isClosed_ge' + +theorem isClosed_Ici {a : α} : IsClosed (Ici a) := + isClosed_ge' a +#align is_closed_Ici isClosed_Ici + +instance : OrderClosedTopology αᵒᵈ := + ⟨(@OrderClosedTopology.isClosed_le' α _ _ _).preimage continuous_swap⟩ + +theorem isClosed_Icc {a b : α} : IsClosed (Icc a b) := + IsClosed.inter isClosed_Ici isClosed_Iic +#align is_closed_Icc isClosed_Icc + +@[simp] +theorem closure_Icc (a b : α) : closure (Icc a b) = Icc a b := + isClosed_Icc.closure_eq +#align closure_Icc closure_Icc + +@[simp] +theorem closure_Iic (a : α) : closure (Iic a) = Iic a := + isClosed_Iic.closure_eq +#align closure_Iic closure_Iic + +@[simp] +theorem closure_Ici (a : α) : closure (Ici a) = Ici a := + isClosed_Ici.closure_eq +#align closure_Ici closure_Ici + +theorem le_of_tendsto_of_tendsto {f g : β → α} {b : Filter β} {a₁ a₂ : α} [NeBot b] + (hf : Tendsto f b (𝓝 a₁)) (hg : Tendsto g b (𝓝 a₂)) (h : f ≤ᶠ[b] g) : a₁ ≤ a₂ := + have : Tendsto (fun b => (f b, g b)) b (𝓝 (a₁, a₂)) := hf.prod_mk_nhds hg + show (a₁, a₂) ∈ { p : α × α | p.1 ≤ p.2 } from t.isClosed_le'.mem_of_tendsto this h +#align le_of_tendsto_of_tendsto le_of_tendsto_of_tendsto + +alias le_of_tendsto_of_tendsto ← tendsto_le_of_eventuallyLe +#align tendsto_le_of_eventually_le tendsto_le_of_eventuallyLe + +theorem le_of_tendsto_of_tendsto' {f g : β → α} {b : Filter β} {a₁ a₂ : α} [NeBot b] + (hf : Tendsto f b (𝓝 a₁)) (hg : Tendsto g b (𝓝 a₂)) (h : ∀ x, f x ≤ g x) : a₁ ≤ a₂ := + le_of_tendsto_of_tendsto hf hg (eventually_of_forall h) +#align le_of_tendsto_of_tendsto' le_of_tendsto_of_tendsto' + +theorem le_of_tendsto {f : β → α} {a b : α} {x : Filter β} [NeBot x] (lim : Tendsto f x (𝓝 a)) + (h : ∀ᶠ c in x, f c ≤ b) : a ≤ b := + le_of_tendsto_of_tendsto lim tendsto_const_nhds h +#align le_of_tendsto le_of_tendsto + +theorem le_of_tendsto' {f : β → α} {a b : α} {x : Filter β} [NeBot x] (lim : Tendsto f x (𝓝 a)) + (h : ∀ c, f c ≤ b) : a ≤ b := + le_of_tendsto lim (eventually_of_forall h) +#align le_of_tendsto' le_of_tendsto' + +theorem ge_of_tendsto {f : β → α} {a b : α} {x : Filter β} [NeBot x] (lim : Tendsto f x (𝓝 a)) + (h : ∀ᶠ c in x, b ≤ f c) : b ≤ a := + le_of_tendsto_of_tendsto tendsto_const_nhds lim h +#align ge_of_tendsto ge_of_tendsto + +theorem ge_of_tendsto' {f : β → α} {a b : α} {x : Filter β} [NeBot x] (lim : Tendsto f x (𝓝 a)) + (h : ∀ c, b ≤ f c) : b ≤ a := + ge_of_tendsto lim (eventually_of_forall h) +#align ge_of_tendsto' ge_of_tendsto' + +@[simp] +theorem closure_le_eq [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) : + closure { b | f b ≤ g b } = { b | f b ≤ g b } := + (isClosed_le hf hg).closure_eq +#align closure_le_eq closure_le_eq + +theorem closure_lt_subset_le [TopologicalSpace β] {f g : β → α} (hf : Continuous f) + (hg : Continuous g) : closure { b | f b < g b } ⊆ { b | f b ≤ g b } := + (closure_minimal fun _ => le_of_lt) <| isClosed_le hf hg +#align closure_lt_subset_le closure_lt_subset_le + +theorem ContinuousWithinAt.closure_le [TopologicalSpace β] {f g : β → α} {s : Set β} {x : β} + (hx : x ∈ closure s) (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) + (h : ∀ y ∈ s, f y ≤ g y) : f x ≤ g x := + show (f x, g x) ∈ { p : α × α | p.1 ≤ p.2 } from + OrderClosedTopology.isClosed_le'.closure_subset ((hf.prod hg).mem_closure hx h) +#align continuous_within_at.closure_le ContinuousWithinAt.closure_le + +/-- If `s` is a closed set and two functions `f` and `g` are continuous on `s`, +then the set `{x ∈ s | f x ≤ g x}` is a closed set. -/ +theorem IsClosed.isClosed_le [TopologicalSpace β] {f g : β → α} {s : Set β} (hs : IsClosed s) + (hf : ContinuousOn f s) (hg : ContinuousOn g s) : IsClosed ({ x ∈ s | f x ≤ g x }) := + (hf.prod hg).preimage_closed_of_closed hs OrderClosedTopology.isClosed_le' +#align is_closed.is_closed_le IsClosed.isClosed_le + +theorem le_on_closure [TopologicalSpace β] {f g : β → α} {s : Set β} (h : ∀ x ∈ s, f x ≤ g x) + (hf : ContinuousOn f (closure s)) (hg : ContinuousOn g (closure s)) ⦃x⦄ (hx : x ∈ closure s) : + f x ≤ g x := + have : s ⊆ { y ∈ closure s | f y ≤ g y } := fun y hy => ⟨subset_closure hy, h y hy⟩ + (closure_minimal this (isClosed_closure.isClosed_le hf hg) hx).2 +#align le_on_closure le_on_closure + +theorem IsClosed.epigraph [TopologicalSpace β] {f : β → α} {s : Set β} (hs : IsClosed s) + (hf : ContinuousOn f s) : IsClosed { p : β × α | p.1 ∈ s ∧ f p.1 ≤ p.2 } := + (hs.preimage continuous_fst).isClosed_le (hf.comp continuousOn_fst Subset.rfl) continuousOn_snd +#align is_closed.epigraph IsClosed.epigraph + +theorem IsClosed.hypograph [TopologicalSpace β] {f : β → α} {s : Set β} (hs : IsClosed s) + (hf : ContinuousOn f s) : IsClosed { p : β × α | p.1 ∈ s ∧ p.2 ≤ f p.1 } := + (hs.preimage continuous_fst).isClosed_le continuousOn_snd (hf.comp continuousOn_fst Subset.rfl) +#align is_closed.hypograph IsClosed.hypograph + +-- todo: move these lemmas to `Topology.Algebra.Order.LeftRight` +theorem nhdsWithin_Ici_neBot {a b : α} (H₂ : a ≤ b) : NeBot (𝓝[Ici a] b) := + nhdsWithin_neBot_of_mem H₂ +#align nhds_within_Ici_ne_bot nhdsWithin_Ici_neBot + +@[instance] +theorem nhdsWithin_Ici_self_neBot (a : α) : NeBot (𝓝[≥] a) := + nhdsWithin_Ici_neBot (le_refl a) +#align nhds_within_Ici_self_ne_bot nhdsWithin_Ici_self_neBot + +theorem nhdsWithin_Iic_neBot {a b : α} (H : a ≤ b) : NeBot (𝓝[Iic b] a) := + nhdsWithin_neBot_of_mem H +#align nhds_within_Iic_ne_bot nhdsWithin_Iic_neBot + +@[instance] +theorem nhdsWithin_Iic_self_neBot (a : α) : NeBot (𝓝[≤] a) := + nhdsWithin_Iic_neBot (le_refl a) +#align nhds_within_Iic_self_ne_bot nhdsWithin_Iic_self_neBot + +end Preorder + +section PartialOrder + +variable [TopologicalSpace α] [PartialOrder α] [t : OrderClosedTopology α] + +-- see Note [lower instance priority] +instance (priority := 90) OrderClosedTopology.to_t2Space : T2Space α := + t2_iff_isClosed_diagonal.2 <| by + simpa only [diagonal, le_antisymm_iff] using + t.isClosed_le'.inter (isClosed_le continuous_snd continuous_fst) +#align order_closed_topology.to_t2_space OrderClosedTopology.to_t2Space + +end PartialOrder + +section LinearOrder + +variable [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] + +theorem isOpen_lt [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) : + IsOpen { b | f b < g b } := by + simpa only [lt_iff_not_le] using (isClosed_le hg hf).isOpen_compl +#align is_open_lt isOpen_lt + +theorem isOpen_lt_prod : IsOpen { p : α × α | p.1 < p.2 } := + isOpen_lt continuous_fst continuous_snd +#align is_open_lt_prod isOpen_lt_prod + +variable {a b : α} + +theorem isOpen_Iio : IsOpen (Iio a) := + isOpen_lt continuous_id continuous_const +#align is_open_Iio isOpen_Iio + +theorem isOpen_Ioi : IsOpen (Ioi a) := + isOpen_lt continuous_const continuous_id +#align is_open_Ioi isOpen_Ioi + +theorem isOpen_Ioo : IsOpen (Ioo a b) := + IsOpen.inter isOpen_Ioi isOpen_Iio +#align is_open_Ioo isOpen_Ioo + +@[simp] +theorem interior_Ioi : interior (Ioi a) = Ioi a := + isOpen_Ioi.interior_eq +#align interior_Ioi interior_Ioi + +@[simp] +theorem interior_Iio : interior (Iio a) = Iio a := + isOpen_Iio.interior_eq +#align interior_Iio interior_Iio + +@[simp] +theorem interior_Ioo : interior (Ioo a b) = Ioo a b := + isOpen_Ioo.interior_eq +#align interior_Ioo interior_Ioo + +theorem Ioo_subset_closure_interior : Ioo a b ⊆ closure (interior (Ioo a b)) := by + simp only [interior_Ioo, subset_closure] +#align Ioo_subset_closure_interior Ioo_subset_closure_interior + +theorem Iio_mem_nhds {a b : α} (h : a < b) : Iio b ∈ 𝓝 a := + IsOpen.mem_nhds isOpen_Iio h +#align Iio_mem_nhds Iio_mem_nhds + +theorem Ioi_mem_nhds {a b : α} (h : a < b) : Ioi a ∈ 𝓝 b := + IsOpen.mem_nhds isOpen_Ioi h +#align Ioi_mem_nhds Ioi_mem_nhds + +theorem Iic_mem_nhds {a b : α} (h : a < b) : Iic b ∈ 𝓝 a := + mem_of_superset (Iio_mem_nhds h) Iio_subset_Iic_self +#align Iic_mem_nhds Iic_mem_nhds + +theorem Ici_mem_nhds {a b : α} (h : a < b) : Ici a ∈ 𝓝 b := + mem_of_superset (Ioi_mem_nhds h) Ioi_subset_Ici_self +#align Ici_mem_nhds Ici_mem_nhds + +theorem Ioo_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Ioo a b ∈ 𝓝 x := + IsOpen.mem_nhds isOpen_Ioo ⟨ha, hb⟩ +#align Ioo_mem_nhds Ioo_mem_nhds + +theorem Ioc_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Ioc a b ∈ 𝓝 x := + mem_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Ioc_self +#align Ioc_mem_nhds Ioc_mem_nhds + +theorem Ico_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Ico a b ∈ 𝓝 x := + mem_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Ico_self +#align Ico_mem_nhds Ico_mem_nhds + +theorem Icc_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Icc a b ∈ 𝓝 x := + mem_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Icc_self +#align Icc_mem_nhds Icc_mem_nhds + +theorem eventually_lt_of_tendsto_lt {l : Filter γ} {f : γ → α} {u v : α} (hv : v < u) + (h : Filter.Tendsto f l (𝓝 v)) : ∀ᶠ a in l, f a < u := + tendsto_nhds.1 h (· < u) isOpen_Iio hv +#align eventually_lt_of_tendsto_lt eventually_lt_of_tendsto_lt + +theorem eventually_gt_of_tendsto_gt {l : Filter γ} {f : γ → α} {u v : α} (hv : u < v) + (h : Filter.Tendsto f l (𝓝 v)) : ∀ᶠ a in l, u < f a := + tendsto_nhds.1 h (· > u) isOpen_Ioi hv +#align eventually_gt_of_tendsto_gt eventually_gt_of_tendsto_gt + +theorem eventually_le_of_tendsto_lt {l : Filter γ} {f : γ → α} {u v : α} (hv : v < u) + (h : Tendsto f l (𝓝 v)) : ∀ᶠ a in l, f a ≤ u := + (eventually_lt_of_tendsto_lt hv h).mono fun _ => le_of_lt +#align eventually_le_of_tendsto_lt eventually_le_of_tendsto_lt + +theorem eventually_ge_of_tendsto_gt {l : Filter γ} {f : γ → α} {u v : α} (hv : u < v) + (h : Tendsto f l (𝓝 v)) : ∀ᶠ a in l, u ≤ f a := + (eventually_gt_of_tendsto_gt hv h).mono fun _ => le_of_lt +#align eventually_ge_of_tendsto_gt eventually_ge_of_tendsto_gt + +variable [TopologicalSpace γ] + +/-! +### Neighborhoods to the left and to the right on an `OrderClosedTopology` + +Limits to the left and to the right of real functions are defined in terms of neighborhoods to +the left and to the right, either open or closed, i.e., members of `𝓝[>] a` and +`𝓝[≥] a` on the right, and similarly on the left. Here we simply prove that all +right-neighborhoods of a point are equal, and we'll prove later other useful characterizations which +require the stronger hypothesis `OrderTopology α` -/ + + +/-! +#### Right neighborhoods, point excluded +-/ + +theorem Ioo_mem_nhdsWithin_Ioi {a b c : α} (H : b ∈ Ico a c) : Ioo a c ∈ 𝓝[>] b := + mem_nhdsWithin.2 + ⟨Iio c, isOpen_Iio, H.2, by rw [inter_comm, Ioi_inter_Iio]; exact Ioo_subset_Ioo_left H.1⟩ +#align Ioo_mem_nhds_within_Ioi Ioo_mem_nhdsWithin_Ioi + +-- porting note: new lemma; todo: swap `'`? +theorem Ioo_mem_nhdsWithin_Ioi' {a b : α} (H : a < b) : Ioo a b ∈ 𝓝[>] a := + Ioo_mem_nhdsWithin_Ioi ⟨le_rfl, H⟩ + +theorem Ioc_mem_nhdsWithin_Ioi {a b c : α} (H : b ∈ Ico a c) : Ioc a c ∈ 𝓝[>] b := + mem_of_superset (Ioo_mem_nhdsWithin_Ioi H) Ioo_subset_Ioc_self +#align Ioc_mem_nhds_within_Ioi Ioc_mem_nhdsWithin_Ioi + +-- porting note: new lemma; todo: swap `'`? +theorem Ioc_mem_nhdsWithin_Ioi' {a b : α} (H : a < b) : Ioc a b ∈ 𝓝[>] a := + Ioc_mem_nhdsWithin_Ioi ⟨le_rfl, H⟩ + +theorem Ico_mem_nhdsWithin_Ioi {a b c : α} (H : b ∈ Ico a c) : Ico a c ∈ 𝓝[>] b := + mem_of_superset (Ioo_mem_nhdsWithin_Ioi H) Ioo_subset_Ico_self +#align Ico_mem_nhds_within_Ioi Ico_mem_nhdsWithin_Ioi + +-- porting note: new lemma; todo: swap `'`? +theorem Ico_mem_nhdsWithin_Ioi' {a b : α} (H : a < b) : Ico a b ∈ 𝓝[>] a := + Ico_mem_nhdsWithin_Ioi ⟨le_rfl, H⟩ + +theorem Icc_mem_nhdsWithin_Ioi {a b c : α} (H : b ∈ Ico a c) : Icc a c ∈ 𝓝[>] b := + mem_of_superset (Ioo_mem_nhdsWithin_Ioi H) Ioo_subset_Icc_self +#align Icc_mem_nhds_within_Ioi Icc_mem_nhdsWithin_Ioi + +-- porting note: new lemma; todo: swap `'`? +theorem Icc_mem_nhdsWithin_Ioi' {a b : α} (H : a < b) : Icc a b ∈ 𝓝[>] a := + Icc_mem_nhdsWithin_Ioi ⟨le_rfl, H⟩ + +@[simp] +theorem nhdsWithin_Ioc_eq_nhdsWithin_Ioi {a b : α} (h : a < b) : 𝓝[Ioc a b] a = 𝓝[>] a := + nhdsWithin_inter_of_mem' <| nhdsWithin_le_nhds <| Iic_mem_nhds h +#align nhds_within_Ioc_eq_nhds_within_Ioi nhdsWithin_Ioc_eq_nhdsWithin_Ioi + +@[simp] +theorem nhdsWithin_Ioo_eq_nhdsWithin_Ioi {a b : α} (h : a < b) : 𝓝[Ioo a b] a = 𝓝[>] a := + nhdsWithin_inter_of_mem' <| nhdsWithin_le_nhds <| Iio_mem_nhds h +#align nhds_within_Ioo_eq_nhds_within_Ioi nhdsWithin_Ioo_eq_nhdsWithin_Ioi + +@[simp] +theorem continuousWithinAt_Ioc_iff_Ioi [TopologicalSpace β] {a b : α} {f : α → β} (h : a < b) : + ContinuousWithinAt f (Ioc a b) a ↔ ContinuousWithinAt f (Ioi a) a := by + simp only [ContinuousWithinAt, nhdsWithin_Ioc_eq_nhdsWithin_Ioi h] +#align continuous_within_at_Ioc_iff_Ioi continuousWithinAt_Ioc_iff_Ioi + +@[simp] +theorem continuousWithinAt_Ioo_iff_Ioi [TopologicalSpace β] {a b : α} {f : α → β} (h : a < b) : + ContinuousWithinAt f (Ioo a b) a ↔ ContinuousWithinAt f (Ioi a) a := by + simp only [ContinuousWithinAt, nhdsWithin_Ioo_eq_nhdsWithin_Ioi h] +#align continuous_within_at_Ioo_iff_Ioi continuousWithinAt_Ioo_iff_Ioi + +/-! +#### Left neighborhoods, point excluded +-/ + +theorem Ioo_mem_nhdsWithin_Iio {a b c : α} (H : b ∈ Ioc a c) : Ioo a c ∈ 𝓝[<] b := by + simpa only [dual_Ioo] using + Ioo_mem_nhdsWithin_Ioi (show toDual b ∈ Ico (toDual c) (toDual a) from H.symm) +#align Ioo_mem_nhds_within_Iio Ioo_mem_nhdsWithin_Iio + +-- porting note: new lemma; todo: swap `'`? +theorem Ioo_mem_nhdsWithin_Iio' {a b : α} (H : a < b) : Ioo a b ∈ 𝓝[<] b := + Ioo_mem_nhdsWithin_Iio ⟨H, le_rfl⟩ + +theorem Ico_mem_nhdsWithin_Iio {a b c : α} (H : b ∈ Ioc a c) : Ico a c ∈ 𝓝[<] b := + mem_of_superset (Ioo_mem_nhdsWithin_Iio H) Ioo_subset_Ico_self +#align Ico_mem_nhds_within_Iio Ico_mem_nhdsWithin_Iio + +-- porting note: new lemma; todo: swap `'`? +theorem Ico_mem_nhdsWithin_Iio' {a b : α} (H : a < b) : Ico a b ∈ 𝓝[<] b := + Ico_mem_nhdsWithin_Iio ⟨H, le_rfl⟩ + +theorem Ioc_mem_nhdsWithin_Iio {a b c : α} (H : b ∈ Ioc a c) : Ioc a c ∈ 𝓝[<] b := + mem_of_superset (Ioo_mem_nhdsWithin_Iio H) Ioo_subset_Ioc_self +#align Ioc_mem_nhds_within_Iio Ioc_mem_nhdsWithin_Iio + +-- porting note: new lemma; todo: swap `'`? +theorem Ioc_mem_nhdsWithin_Iio' {a b : α} (H : a < b) : Ioc a b ∈ 𝓝[<] b := + Ioc_mem_nhdsWithin_Iio ⟨H, le_rfl⟩ + +theorem Icc_mem_nhdsWithin_Iio {a b c : α} (H : b ∈ Ioc a c) : Icc a c ∈ 𝓝[<] b := + mem_of_superset (Ioo_mem_nhdsWithin_Iio H) Ioo_subset_Icc_self +#align Icc_mem_nhds_within_Iio Icc_mem_nhdsWithin_Iio + +theorem Icc_mem_nhdsWithin_Iio' {a b : α} (H : a < b) : Icc a b ∈ 𝓝[<] b := + Icc_mem_nhdsWithin_Iio ⟨H, le_rfl⟩ + +@[simp] +theorem nhdsWithin_Ico_eq_nhdsWithin_Iio {a b : α} (h : a < b) : 𝓝[Ico a b] b = 𝓝[<] b := by + simpa only [dual_Ioc] using nhdsWithin_Ioc_eq_nhdsWithin_Ioi h.dual +#align nhds_within_Ico_eq_nhds_within_Iio nhdsWithin_Ico_eq_nhdsWithin_Iio + +@[simp] +theorem nhdsWithin_Ioo_eq_nhdsWithin_Iio {a b : α} (h : a < b) : 𝓝[Ioo a b] b = 𝓝[<] b := by + simpa only [dual_Ioo] using nhdsWithin_Ioo_eq_nhdsWithin_Ioi h.dual +#align nhds_within_Ioo_eq_nhds_within_Iio nhdsWithin_Ioo_eq_nhdsWithin_Iio + +@[simp] +theorem continuousWithinAt_Ico_iff_Iio {a b : α} {f : α → γ} (h : a < b) : + ContinuousWithinAt f (Ico a b) b ↔ ContinuousWithinAt f (Iio b) b := by + simp only [ContinuousWithinAt, nhdsWithin_Ico_eq_nhdsWithin_Iio h] +#align continuous_within_at_Ico_iff_Iio continuousWithinAt_Ico_iff_Iio + +@[simp] +theorem continuousWithinAt_Ioo_iff_Iio {a b : α} {f : α → γ} (h : a < b) : + ContinuousWithinAt f (Ioo a b) b ↔ ContinuousWithinAt f (Iio b) b := by + simp only [ContinuousWithinAt, nhdsWithin_Ioo_eq_nhdsWithin_Iio h] +#align continuous_within_at_Ioo_iff_Iio continuousWithinAt_Ioo_iff_Iio + +/-! +#### Right neighborhoods, point included +-/ + +theorem Ioo_mem_nhdsWithin_Ici {a b c : α} (H : b ∈ Ioo a c) : Ioo a c ∈ 𝓝[≥] b := + mem_nhdsWithin_of_mem_nhds <| IsOpen.mem_nhds isOpen_Ioo H +#align Ioo_mem_nhds_within_Ici Ioo_mem_nhdsWithin_Ici + +theorem Ioc_mem_nhdsWithin_Ici {a b c : α} (H : b ∈ Ioo a c) : Ioc a c ∈ 𝓝[≥] b := + mem_of_superset (Ioo_mem_nhdsWithin_Ici H) Ioo_subset_Ioc_self +#align Ioc_mem_nhds_within_Ici Ioc_mem_nhdsWithin_Ici + +theorem Ico_mem_nhdsWithin_Ici {a b c : α} (H : b ∈ Ico a c) : Ico a c ∈ 𝓝[≥] b := + mem_nhdsWithin.2 + ⟨Iio c, isOpen_Iio, H.2, by simp only [inter_comm, Ici_inter_Iio, Ico_subset_Ico_left H.1]⟩ +#align Ico_mem_nhds_within_Ici Ico_mem_nhdsWithin_Ici + +theorem Ico_mem_nhdsWithin_Ici' {a b : α} (H : a < b) : Ico a b ∈ 𝓝[≥] a := + Ico_mem_nhdsWithin_Ici ⟨le_rfl, H⟩ + +theorem Icc_mem_nhdsWithin_Ici {a b c : α} (H : b ∈ Ico a c) : Icc a c ∈ 𝓝[≥] b := + mem_of_superset (Ico_mem_nhdsWithin_Ici H) Ico_subset_Icc_self +#align Icc_mem_nhds_within_Ici Icc_mem_nhdsWithin_Ici + +theorem Icc_mem_nhdsWithin_Ici' {a b : α} (H : a < b) : Icc a b ∈ 𝓝[≥] a := + Icc_mem_nhdsWithin_Ici ⟨le_rfl, H⟩ + +@[simp] +theorem nhdsWithin_Icc_eq_nhdsWithin_Ici {a b : α} (h : a < b) : 𝓝[Icc a b] a = 𝓝[≥] a := + nhdsWithin_inter_of_mem' <| nhdsWithin_le_nhds <| Iic_mem_nhds h +#align nhds_within_Icc_eq_nhds_within_Ici nhdsWithin_Icc_eq_nhdsWithin_Ici + +@[simp] +theorem nhdsWithin_Ico_eq_nhdsWithin_Ici {a b : α} (h : a < b) : 𝓝[Ico a b] a = 𝓝[≥] a := + nhdsWithin_inter_of_mem' <| nhdsWithin_le_nhds <| Iio_mem_nhds h +#align nhds_within_Ico_eq_nhds_within_Ici nhdsWithin_Ico_eq_nhdsWithin_Ici + +@[simp] +theorem continuousWithinAt_Icc_iff_Ici [TopologicalSpace β] {a b : α} {f : α → β} (h : a < b) : + ContinuousWithinAt f (Icc a b) a ↔ ContinuousWithinAt f (Ici a) a := by + simp only [ContinuousWithinAt, nhdsWithin_Icc_eq_nhdsWithin_Ici h] +#align continuous_within_at_Icc_iff_Ici continuousWithinAt_Icc_iff_Ici + +@[simp] +theorem continuousWithinAt_Ico_iff_Ici [TopologicalSpace β] {a b : α} {f : α → β} (h : a < b) : + ContinuousWithinAt f (Ico a b) a ↔ ContinuousWithinAt f (Ici a) a := by + simp only [ContinuousWithinAt, nhdsWithin_Ico_eq_nhdsWithin_Ici h] +#align continuous_within_at_Ico_iff_Ici continuousWithinAt_Ico_iff_Ici + +/-! +#### Left neighborhoods, point included +-/ + + +theorem Ioo_mem_nhdsWithin_Iic {a b c : α} (H : b ∈ Ioo a c) : Ioo a c ∈ 𝓝[≤] b := + mem_nhdsWithin_of_mem_nhds <| IsOpen.mem_nhds isOpen_Ioo H +#align Ioo_mem_nhds_within_Iic Ioo_mem_nhdsWithin_Iic + +theorem Ico_mem_nhdsWithin_Iic {a b c : α} (H : b ∈ Ioo a c) : Ico a c ∈ 𝓝[≤] b := + mem_of_superset (Ioo_mem_nhdsWithin_Iic H) Ioo_subset_Ico_self +#align Ico_mem_nhds_within_Iic Ico_mem_nhdsWithin_Iic + +theorem Ioc_mem_nhdsWithin_Iic {a b c : α} (H : b ∈ Ioc a c) : Ioc a c ∈ 𝓝[≤] b := by + simpa only [dual_Ico] using + Ico_mem_nhdsWithin_Ici (show toDual b ∈ Ico (toDual c) (toDual a) from H.symm) +#align Ioc_mem_nhds_within_Iic Ioc_mem_nhdsWithin_Iic + +theorem Ioc_mem_nhdsWithin_Iic' {a b : α} (H : a < b) : Ioc a b ∈ 𝓝[≤] b := + Ioc_mem_nhdsWithin_Iic ⟨H, le_rfl⟩ + +theorem Icc_mem_nhdsWithin_Iic {a b c : α} (H : b ∈ Ioc a c) : Icc a c ∈ 𝓝[≤] b := + mem_of_superset (Ioc_mem_nhdsWithin_Iic H) Ioc_subset_Icc_self +#align Icc_mem_nhds_within_Iic Icc_mem_nhdsWithin_Iic + +theorem Icc_mem_nhdsWithin_Iic' {a b : α} (H : a < b) : Icc a b ∈ 𝓝[≤] b := + Icc_mem_nhdsWithin_Iic ⟨H, le_rfl⟩ + +@[simp] +theorem nhdsWithin_Icc_eq_nhdsWithin_Iic {a b : α} (h : a < b) : 𝓝[Icc a b] b = 𝓝[≤] b := by + simpa only [dual_Icc] using nhdsWithin_Icc_eq_nhdsWithin_Ici h.dual +#align nhds_within_Icc_eq_nhds_within_Iic nhdsWithin_Icc_eq_nhdsWithin_Iic + +@[simp] +theorem nhdsWithin_Ioc_eq_nhdsWithin_Iic {a b : α} (h : a < b) : 𝓝[Ioc a b] b = 𝓝[≤] b := by + simpa only [dual_Ico] using nhdsWithin_Ico_eq_nhdsWithin_Ici h.dual +#align nhds_within_Ioc_eq_nhds_within_Iic nhdsWithin_Ioc_eq_nhdsWithin_Iic + +@[simp] +theorem continuousWithinAt_Icc_iff_Iic [TopologicalSpace β] {a b : α} {f : α → β} (h : a < b) : + ContinuousWithinAt f (Icc a b) b ↔ ContinuousWithinAt f (Iic b) b := by + simp only [ContinuousWithinAt, nhdsWithin_Icc_eq_nhdsWithin_Iic h] +#align continuous_within_at_Icc_iff_Iic continuousWithinAt_Icc_iff_Iic + +@[simp] +theorem continuousWithinAt_Ioc_iff_Iic [TopologicalSpace β] {a b : α} {f : α → β} (h : a < b) : + ContinuousWithinAt f (Ioc a b) b ↔ ContinuousWithinAt f (Iic b) b := by + simp only [ContinuousWithinAt, nhdsWithin_Ioc_eq_nhdsWithin_Iic h] +#align continuous_within_at_Ioc_iff_Iic continuousWithinAt_Ioc_iff_Iic + +end LinearOrder + +section LinearOrder + +variable [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f g : β → α} + +section + +variable [TopologicalSpace β] + +theorem lt_subset_interior_le (hf : Continuous f) (hg : Continuous g) : + { b | f b < g b } ⊆ interior { b | f b ≤ g b } := + (interior_maximal fun _ => le_of_lt) <| isOpen_lt hf hg +#align lt_subset_interior_le lt_subset_interior_le + +theorem frontier_le_subset_eq (hf : Continuous f) (hg : Continuous g) : + frontier { b | f b ≤ g b } ⊆ { b | f b = g b } := by + rw [frontier_eq_closure_inter_closure, closure_le_eq hf hg] + rintro b ⟨hb₁, hb₂⟩ + refine' le_antisymm hb₁ (closure_lt_subset_le hg hf _) + convert hb₂ using 2; simp only [not_le.symm]; rfl +#align frontier_le_subset_eq frontier_le_subset_eq + +theorem frontier_Iic_subset (a : α) : frontier (Iic a) ⊆ {a} := + frontier_le_subset_eq (@continuous_id α _) continuous_const +#align frontier_Iic_subset frontier_Iic_subset + +theorem frontier_Ici_subset (a : α) : frontier (Ici a) ⊆ {a} := + @frontier_Iic_subset αᵒᵈ _ _ _ _ +#align frontier_Ici_subset frontier_Ici_subset + +theorem frontier_lt_subset_eq (hf : Continuous f) (hg : Continuous g) : + frontier { b | f b < g b } ⊆ { b | f b = g b } := by + simpa only [← not_lt, ← compl_setOf, frontier_compl, eq_comm] using frontier_le_subset_eq hg hf +#align frontier_lt_subset_eq frontier_lt_subset_eq + +theorem continuous_if_le [TopologicalSpace γ] [∀ x, Decidable (f x ≤ g x)] {f' g' : β → γ} + (hf : Continuous f) (hg : Continuous g) (hf' : ContinuousOn f' { x | f x ≤ g x }) + (hg' : ContinuousOn g' { x | g x ≤ f x }) (hfg : ∀ x, f x = g x → f' x = g' x) : + Continuous fun x => if f x ≤ g x then f' x else g' x := by + refine' continuous_if (fun a ha => hfg _ (frontier_le_subset_eq hf hg ha)) _ (hg'.mono _) + · rwa [(isClosed_le hf hg).closure_eq] + · simp only [not_le] + exact closure_lt_subset_le hg hf +#align continuous_if_le continuous_if_le + +theorem Continuous.if_le [TopologicalSpace γ] [∀ x, Decidable (f x ≤ g x)] {f' g' : β → γ} + (hf' : Continuous f') (hg' : Continuous g') (hf : Continuous f) (hg : Continuous g) + (hfg : ∀ x, f x = g x → f' x = g' x) : Continuous fun x => if f x ≤ g x then f' x else g' x := + continuous_if_le hf hg hf'.continuousOn hg'.continuousOn hfg +#align continuous.if_le Continuous.if_le + +theorem Filter.Tendsto.eventually_lt {l : Filter γ} {f g : γ → α} {y z : α} (hf : Tendsto f l (𝓝 y)) + (hg : Tendsto g l (𝓝 z)) (hyz : y < z) : ∀ᶠ x in l, f x < g x := + let ⟨_a, ha, _b, hb, h⟩ := hyz.exists_disjoint_Iio_Ioi + (hg.eventually (Ioi_mem_nhds hb)).mp <| (hf.eventually (Iio_mem_nhds ha)).mono fun _ h₁ h₂ => + h _ h₁ _ h₂ +#align tendsto.eventually_lt Filter.Tendsto.eventually_lt + +nonrec theorem ContinuousAt.eventually_lt {x₀ : β} (hf : ContinuousAt f x₀) (hg : ContinuousAt g x₀) + (hfg : f x₀ < g x₀) : ∀ᶠ x in 𝓝 x₀, f x < g x := + hf.eventually_lt hg hfg +#align continuous_at.eventually_lt ContinuousAt.eventually_lt + +-- porting note: todo: restore @[continuity] +protected theorem Continuous.min (hf : Continuous f) (hg : Continuous g) : + Continuous fun b => min (f b) (g b) := by + simp only [min_def] + exact hf.if_le hg hf hg fun x => id +#align continuous.min Continuous.min + +-- porting note: todo: restore @[continuity] +protected theorem Continuous.max (hf : Continuous f) (hg : Continuous g) : + Continuous fun b => max (f b) (g b) := + @Continuous.min αᵒᵈ _ _ _ _ _ _ _ hf hg +#align continuous.max Continuous.max + +end + +theorem continuous_min : Continuous fun p : α × α => min p.1 p.2 := + continuous_fst.min continuous_snd +#align continuous_min continuous_min + +theorem continuous_max : Continuous fun p : α × α => max p.1 p.2 := + continuous_fst.max continuous_snd +#align continuous_max continuous_max + +protected theorem Filter.Tendsto.max {b : Filter β} {a₁ a₂ : α} (hf : Tendsto f b (𝓝 a₁)) + (hg : Tendsto g b (𝓝 a₂)) : Tendsto (fun b => max (f b) (g b)) b (𝓝 (max a₁ a₂)) := + (continuous_max.tendsto (a₁, a₂)).comp (hf.prod_mk_nhds hg) +#align filter.tendsto.max Filter.Tendsto.max + +protected theorem Filter.Tendsto.min {b : Filter β} {a₁ a₂ : α} (hf : Tendsto f b (𝓝 a₁)) + (hg : Tendsto g b (𝓝 a₂)) : Tendsto (fun b => min (f b) (g b)) b (𝓝 (min a₁ a₂)) := + (continuous_min.tendsto (a₁, a₂)).comp (hf.prod_mk_nhds hg) +#align filter.tendsto.min Filter.Tendsto.min + +protected theorem Filter.Tendsto.max_right {l : Filter β} {a : α} (h : Tendsto f l (𝓝 a)) : + Tendsto (fun i => max a (f i)) l (𝓝 a) := by + convert ((continuous_max.comp (@Continuous.Prod.mk α α _ _ a)).tendsto a).comp h + simp +#align filter.tendsto.max_right Filter.Tendsto.max_right + +protected theorem Filter.Tendsto.max_left {l : Filter β} {a : α} (h : Tendsto f l (𝓝 a)) : + Tendsto (fun i => max (f i) a) l (𝓝 a) := by + simp_rw [max_comm _ a] + exact h.max_right +#align filter.tendsto.max_left Filter.Tendsto.max_left + +theorem Filter.tendsto_nhds_max_right {l : Filter β} {a : α} (h : Tendsto f l (𝓝[>] a)) : + Tendsto (fun i => max a (f i)) l (𝓝[>] a) := by + obtain ⟨h₁ : Tendsto f l (𝓝 a), h₂ : ∀ᶠ i in l, f i ∈ Ioi a⟩ := tendsto_nhdsWithin_iff.mp h + exact tendsto_nhdsWithin_iff.mpr ⟨h₁.max_right, h₂.mono fun i hi => lt_max_of_lt_right hi⟩ +#align filter.tendsto_nhds_max_right Filter.tendsto_nhds_max_right + +theorem Filter.tendsto_nhds_max_left {l : Filter β} {a : α} (h : Tendsto f l (𝓝[>] a)) : + Tendsto (fun i => max (f i) a) l (𝓝[>] a) := by + simp_rw [max_comm _ a] + exact Filter.tendsto_nhds_max_right h +#align filter.tendsto_nhds_max_left Filter.tendsto_nhds_max_left + +theorem Filter.Tendsto.min_right {l : Filter β} {a : α} (h : Tendsto f l (𝓝 a)) : + Tendsto (fun i => min a (f i)) l (𝓝 a) := + @Filter.Tendsto.max_right αᵒᵈ β _ _ _ f l a h +#align filter.tendsto.min_right Filter.Tendsto.min_right + +theorem Filter.Tendsto.min_left {l : Filter β} {a : α} (h : Tendsto f l (𝓝 a)) : + Tendsto (fun i => min (f i) a) l (𝓝 a) := + @Filter.Tendsto.max_left αᵒᵈ β _ _ _ f l a h +#align filter.tendsto.min_left Filter.Tendsto.min_left + +theorem Filter.tendsto_nhds_min_right {l : Filter β} {a : α} (h : Tendsto f l (𝓝[<] a)) : + Tendsto (fun i => min a (f i)) l (𝓝[<] a) := + @Filter.tendsto_nhds_max_right αᵒᵈ β _ _ _ f l a h +#align filter.tendsto_nhds_min_right Filter.tendsto_nhds_min_right + +theorem Filter.tendsto_nhds_min_left {l : Filter β} {a : α} (h : Tendsto f l (𝓝[<] a)) : + Tendsto (fun i => min (f i) a) l (𝓝[<] a) := + @Filter.tendsto_nhds_max_left αᵒᵈ β _ _ _ f l a h +#align filter.tendsto_nhds_min_left Filter.tendsto_nhds_min_left + +protected theorem Dense.exists_lt [NoMinOrder α] {s : Set α} (hs : Dense s) (x : α) : + ∃ y ∈ s, y < x := + hs.exists_mem_open isOpen_Iio (exists_lt x) +#align dense.exists_lt Dense.exists_lt + +protected theorem Dense.exists_gt [NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) : + ∃ y ∈ s, x < y := + hs.orderDual.exists_lt x +#align dense.exists_gt Dense.exists_gt + +protected theorem Dense.exists_le [NoMinOrder α] {s : Set α} (hs : Dense s) (x : α) : + ∃ y ∈ s, y ≤ x := + (hs.exists_lt x).imp fun _ h => ⟨h.1, h.2.le⟩ +#align dense.exists_le Dense.exists_le + +protected theorem Dense.exists_ge [NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) : + ∃ y ∈ s, x ≤ y := + hs.orderDual.exists_le x +#align dense.exists_ge Dense.exists_ge + +theorem Dense.exists_le' {s : Set α} (hs : Dense s) (hbot : ∀ x, IsBot x → x ∈ s) (x : α) : + ∃ y ∈ s, y ≤ x := by + by_cases hx : IsBot x + · exact ⟨x, hbot x hx, le_rfl⟩ + · simp only [IsBot, not_forall, not_le] at hx + rcases hs.exists_mem_open isOpen_Iio hx with ⟨y, hys, hy : y < x⟩ + exact ⟨y, hys, hy.le⟩ +#align dense.exists_le' Dense.exists_le' + +theorem Dense.exists_ge' {s : Set α} (hs : Dense s) (htop : ∀ x, IsTop x → x ∈ s) (x : α) : + ∃ y ∈ s, x ≤ y := + hs.orderDual.exists_le' htop x +#align dense.exists_ge' Dense.exists_ge' + +theorem Dense.exists_between [DenselyOrdered α] {s : Set α} (hs : Dense s) {x y : α} (h : x < y) : + ∃ z ∈ s, z ∈ Ioo x y := + hs.exists_mem_open isOpen_Ioo (nonempty_Ioo.2 h) +#align dense.exists_between Dense.exists_between + +variable [Nonempty α] [TopologicalSpace β] + +/-- A compact set is bounded below -/ +theorem IsCompact.bddBelow {s : Set α} (hs : IsCompact s) : BddBelow s := by + cases' botOrderOrNoBotOrder α with h h; exact OrderBot.bddBelow s + have : s ⊆ ⋃ a : α, Ioi a := (@unionᵢ_Ioi α _ (NoBotOrder.to_noMinOrder α)).symm ▸ subset_univ s + rcases hs.elim_finite_subcover _ (fun _ => isOpen_Ioi) this with ⟨t, ht⟩ + refine t.bddBelow.imp fun C hC y hy => ?_ + rcases mem_unionᵢ₂.1 (ht hy) with ⟨a, ha, hay⟩ + exact (hC ha).trans (le_of_lt hay) +#align is_compact.bdd_below IsCompact.bddBelow + +/-- A compact set is bounded above -/ +theorem IsCompact.bddAbove {s : Set α} (hs : IsCompact s) : BddAbove s := + @IsCompact.bddBelow αᵒᵈ _ _ _ _ _ hs +#align is_compact.bdd_above IsCompact.bddAbove + +/-- A continuous function is bounded below on a compact set. -/ +theorem IsCompact.bddBelow_image {f : β → α} {K : Set β} (hK : IsCompact K) + (hf : ContinuousOn f K) : BddBelow (f '' K) := + (hK.image_of_continuousOn hf).bddBelow +#align is_compact.bdd_below_image IsCompact.bddBelow_image + +/-- A continuous function is bounded above on a compact set. -/ +theorem IsCompact.bddAbove_image {f : β → α} {K : Set β} (hK : IsCompact K) + (hf : ContinuousOn f K) : BddAbove (f '' K) := + @IsCompact.bddBelow_image αᵒᵈ _ _ _ _ _ _ _ _ hK hf +#align is_compact.bdd_above_image IsCompact.bddAbove_image + +/-- A continuous function with compact support is bounded below. -/ +@[to_additive " A continuous function with compact support is bounded below. "] +theorem Continuous.bddBelow_range_of_hasCompactMulSupport [One α] {f : β → α} (hf : Continuous f) + (h : HasCompactMulSupport f) : BddBelow (range f) := + (h.isCompact_range hf).bddBelow +#align continuous.bdd_below_range_of_has_compact_mul_support Continuous.bddBelow_range_of_hasCompactMulSupport +#align continuous.bdd_below_range_of_has_compact_support Continuous.bddBelow_range_of_hasCompactSupport + +/-- A continuous function with compact support is bounded above. -/ +@[to_additive " A continuous function with compact support is bounded above. "] +theorem Continuous.bddAbove_range_of_hasCompactMulSupport [One α] {f : β → α} (hf : Continuous f) + (h : HasCompactMulSupport f) : BddAbove (range f) := + @Continuous.bddBelow_range_of_hasCompactMulSupport αᵒᵈ _ _ _ _ _ _ _ _ hf h +#align continuous.bdd_above_range_of_has_compact_mul_support Continuous.bddAbove_range_of_hasCompactMulSupport +#align continuous.bdd_above_range_of_has_compact_support Continuous.bddAbove_range_of_hasCompactSupport + +end LinearOrder + +end OrderClosedTopology + +instance [Preorder α] [TopologicalSpace α] [OrderClosedTopology α] [Preorder β] [TopologicalSpace β] + [OrderClosedTopology β] : OrderClosedTopology (α × β) := + ⟨(isClosed_le continuous_fst.fst continuous_snd.fst).inter + (isClosed_le continuous_fst.snd continuous_snd.snd)⟩ + +instance {ι : Type _} {α : ι → Type _} [∀ i, Preorder (α i)] [∀ i, TopologicalSpace (α i)] + [∀ i, OrderClosedTopology (α i)] : OrderClosedTopology (∀ i, α i) := by + constructor + simp only [Pi.le_def, setOf_forall] + exact isClosed_interᵢ fun i => isClosed_le (continuous_apply i).fst' (continuous_apply i).snd' + +instance Pi.orderClosedTopology' [Preorder β] [TopologicalSpace β] [OrderClosedTopology β] : + OrderClosedTopology (α → β) := + inferInstance +#align pi.order_closed_topology' Pi.orderClosedTopology' + +-- porting note: todo: define `Preorder.topology` before `OrderTopology` and reuse the def +/-- The order topology on an ordered type is the topology generated by open intervals. We register +it on a preorder, but it is mostly interesting in linear orders, where it is also order-closed. +We define it as a mixin. If you want to introduce the order topology on a preorder, use +`Preorder.topology`. -/ +class OrderTopology (α : Type _) [t : TopologicalSpace α] [Preorder α] : Prop where + /-- The topology is generated by open intervals `Set.Ioi _` and `Set.Iio _`. -/ + topology_eq_generate_intervals : t = generateFrom { s | ∃ a, s = Ioi a ∨ s = Iio a } +#align order_topology OrderTopology + +/-- (Order) topology on a partial order `α` generated by the subbase of open intervals +`(a, ∞) = { x ∣ a < x }, (-∞ , b) = {x ∣ x < b}` for all `a, b` in `α`. We do not register it as an +instance as many ordered sets are already endowed with the same topology, most often in a non-defeq +way though. Register as a local instance when necessary. -/ +def Preorder.topology (α : Type _) [Preorder α] : TopologicalSpace α := + generateFrom { s : Set α | ∃ a : α, s = { b : α | a < b } ∨ s = { b : α | b < a } } +#align preorder.topology Preorder.topology + +section OrderTopology + +section Preorder + +variable [TopologicalSpace α] [Preorder α] [t : OrderTopology α] + +instance : OrderTopology αᵒᵈ := + ⟨by + convert @OrderTopology.topology_eq_generate_intervals α _ _ _ + conv in _ ∨ _ => rw [or_comm]⟩ + +theorem isOpen_iff_generate_intervals {s : Set α} : + IsOpen s ↔ GenerateOpen { s | ∃ a, s = Ioi a ∨ s = Iio a } s := by + rw [t.topology_eq_generate_intervals]; rfl +#align is_open_iff_generate_intervals isOpen_iff_generate_intervals + +theorem isOpen_lt' (a : α) : IsOpen { b : α | a < b } := + isOpen_iff_generate_intervals.2 <| .basic _ ⟨a, .inl rfl⟩ +#align is_open_lt' isOpen_lt' + +theorem isOpen_gt' (a : α) : IsOpen { b : α | b < a } := + isOpen_iff_generate_intervals.2 <| .basic _ ⟨a, .inr rfl⟩ +#align is_open_gt' isOpen_gt' + +theorem lt_mem_nhds {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 b, a < x := + (isOpen_lt' _).mem_nhds h +#align lt_mem_nhds lt_mem_nhds + +theorem le_mem_nhds {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 b, a ≤ x := + (lt_mem_nhds h).mono fun _ => le_of_lt +#align le_mem_nhds le_mem_nhds + +theorem gt_mem_nhds {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 a, x < b := + (isOpen_gt' _).mem_nhds h +#align gt_mem_nhds gt_mem_nhds + +theorem ge_mem_nhds {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 a, x ≤ b := + (gt_mem_nhds h).mono fun _ => le_of_lt +#align ge_mem_nhds ge_mem_nhds + +theorem nhds_eq_order (a : α) : 𝓝 a = (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b) := by + rw [t.topology_eq_generate_intervals, nhds_generateFrom] + simp_rw [mem_setOf_eq, @and_comm (a ∈ _), exists_or, or_and_right, infᵢ_or, infᵢ_and, infᵢ_exists, + infᵢ_inf_eq, infᵢ_comm (ι := Set α), infᵢ_infᵢ_eq_left, mem_Ioi, mem_Iio] +#align nhds_eq_order nhds_eq_order + +theorem tendsto_order {f : β → α} {a : α} {x : Filter β} : + Tendsto f x (𝓝 a) ↔ (∀ a' < a, ∀ᶠ b in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ b in x, f b < a' := by + simp only [nhds_eq_order a, tendsto_inf, tendsto_infᵢ, tendsto_principal]; rfl +#align tendsto_order tendsto_order + +instance tendstoIccClassNhds (a : α) : TendstoIxxClass Icc (𝓝 a) (𝓝 a) := by + simp only [nhds_eq_order, infᵢ_subtype'] + refine + ((hasBasis_infᵢ_principal_finite _).inf (hasBasis_infᵢ_principal_finite _)).tendstoIxxClass + fun s _ => ?_ + refine' ((ordConnected_binterᵢ _).inter (ordConnected_binterᵢ _)).out <;> intro _ _ + exacts [ordConnected_Ioi, ordConnected_Iio] +#align tendsto_Icc_class_nhds tendstoIccClassNhds + +instance tendstoIcoClassNhds (a : α) : TendstoIxxClass Ico (𝓝 a) (𝓝 a) := + tendstoIxxClass_of_subset fun _ _ => Ico_subset_Icc_self +#align tendsto_Ico_class_nhds tendstoIcoClassNhds + +instance tendstoIocClassNhds (a : α) : TendstoIxxClass Ioc (𝓝 a) (𝓝 a) := + tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self +#align tendsto_Ioc_class_nhds tendstoIocClassNhds + +instance tendstoIooClassNhds (a : α) : TendstoIxxClass Ioo (𝓝 a) (𝓝 a) := + tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Icc_self +#align tendsto_Ioo_class_nhds tendstoIooClassNhds + +/-- **Squeeze theorem** (also known as **sandwich theorem**). This version assumes that inequalities +hold eventually for the filter. -/ +theorem tendsto_of_tendsto_of_tendsto_of_le_of_le' {f g h : β → α} {b : Filter β} {a : α} + (hg : Tendsto g b (𝓝 a)) (hh : Tendsto h b (𝓝 a)) (hgf : ∀ᶠ b in b, g b ≤ f b) + (hfh : ∀ᶠ b in b, f b ≤ h b) : Tendsto f b (𝓝 a) := + (hg.Icc hh).of_smallSets <| hgf.and hfh +#align tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_of_tendsto_of_tendsto_of_le_of_le' + +/-- **Squeeze theorem** (also known as **sandwich theorem**). This version assumes that inequalities +hold everywhere. -/ +theorem tendsto_of_tendsto_of_tendsto_of_le_of_le {f g h : β → α} {b : Filter β} {a : α} + (hg : Tendsto g b (𝓝 a)) (hh : Tendsto h b (𝓝 a)) (hgf : g ≤ f) (hfh : f ≤ h) : + Tendsto f b (𝓝 a) := + tendsto_of_tendsto_of_tendsto_of_le_of_le' hg hh (eventually_of_forall hgf) + (eventually_of_forall hfh) +#align tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_of_tendsto_of_tendsto_of_le_of_le + +theorem nhds_order_unbounded {a : α} (hu : ∃ u, a < u) (hl : ∃ l, l < a) : + 𝓝 a = ⨅ (l) (_h₂ : l < a) (u) (_h₂ : a < u), 𝓟 (Ioo l u) := by + simp only [nhds_eq_order, ← inf_binfᵢ, ← binfᵢ_inf, *, ← inf_principal, ← Ioi_inter_Iio]; rfl +#align nhds_order_unbounded nhds_order_unbounded + +theorem tendsto_order_unbounded {f : β → α} {a : α} {x : Filter β} (hu : ∃ u, a < u) + (hl : ∃ l, l < a) (h : ∀ l u, l < a → a < u → ∀ᶠ b in x, l < f b ∧ f b < u) : + Tendsto f x (𝓝 a) := by + simp only [nhds_order_unbounded hu hl, tendsto_infᵢ, tendsto_principal] + exact fun l hl u => h l u hl +#align tendsto_order_unbounded tendsto_order_unbounded + +end Preorder + +instance tendstoIxxNhdsWithin {α : Type _} [Preorder α] [TopologicalSpace α] (a : α) {s t : Set α} + {Ixx} [TendstoIxxClass Ixx (𝓝 a) (𝓝 a)] [TendstoIxxClass Ixx (𝓟 s) (𝓟 t)] : + TendstoIxxClass Ixx (𝓝[s] a) (𝓝[t] a) := + Filter.tendstoIxxClass_inf +#align tendsto_Ixx_nhds_within tendstoIxxNhdsWithin + +instance tendstoIccClassNhdsPi {ι : Type _} {α : ι → Type _} [∀ i, Preorder (α i)] + [∀ i, TopologicalSpace (α i)] [∀ i, OrderTopology (α i)] (f : ∀ i, α i) : + TendstoIxxClass Icc (𝓝 f) (𝓝 f) := by + constructor + conv in (𝓝 f).smallSets => rw [nhds_pi, Filter.pi] + simp only [smallSets_infᵢ, smallSets_comap, tendsto_infᵢ, tendsto_lift', (· ∘ ·), + mem_powerset_iff] + intro i s hs + have : Tendsto (fun g : ∀ i, α i => g i) (𝓝 f) (𝓝 (f i)) := (continuous_apply i).tendsto f + refine' (tendsto_lift'.1 ((this.comp tendsto_fst).Icc (this.comp tendsto_snd)) s hs).mono _ + exact fun p hp g hg => hp ⟨hg.1 _, hg.2 _⟩ +#align tendsto_Icc_class_nhds_pi tendstoIccClassNhdsPi + +-- porting note: new lemma +theorem induced_topology_le_preorder [Preorder α] [Preorder β] [TopologicalSpace β] + [OrderTopology β] {f : α → β} (hf : ∀ {x y}, f x < f y ↔ x < y) : + induced f ‹TopologicalSpace β› ≤ Preorder.topology α := by + let _ := Preorder.topology α; have : OrderTopology α := ⟨rfl⟩ + refine le_of_nhds_le_nhds fun x => ?_ + simp only [nhds_eq_order, nhds_induced, comap_inf, comap_infᵢ, comap_principal, Ioi, Iio, ← hf] + refine inf_le_inf (le_infᵢ₂ fun a ha => ?_) (le_infᵢ₂ fun a ha => ?_) + exacts [infᵢ₂_le (f a) ha, infᵢ₂_le (f a) ha] + +-- porting note: new lemma +theorem induced_topology_eq_preorder [Preorder α] [Preorder β] [TopologicalSpace β] + [OrderTopology β] {f : α → β} (hf : ∀ {x y}, f x < f y ↔ x < y) + (H₁ : ∀ {a b x}, b < f a → ¬(b < f x) → ∃ y, y < a ∧ b ≤ f y) + (H₂ : ∀ {a b x}, f a < b → ¬(f x < b) → ∃ y, a < y ∧ f y ≤ b) : + induced f ‹TopologicalSpace β› = Preorder.topology α := by + let _ := Preorder.topology α; have : OrderTopology α := ⟨rfl⟩ + refine le_antisymm (induced_topology_le_preorder hf) ?_ + refine le_of_nhds_le_nhds fun a => ?_ + simp only [nhds_eq_order, nhds_induced, comap_inf, comap_infᵢ, comap_principal] + refine inf_le_inf (le_infᵢ₂ fun b hb => ?_) (le_infᵢ₂ fun b hb => ?_) + · rcases em (∃ x, ¬(b < f x)) with (⟨x, hx⟩ | hb) + · rcases H₁ hb hx with ⟨y, hya, hyb⟩ + exact infᵢ₂_le_of_le y hya (principal_mono.2 fun z hz => hyb.trans_lt (hf.2 hz)) + · push_neg at hb + exact le_principal_iff.2 (univ_mem' hb) + · rcases em (∃ x, ¬(f x < b)) with (⟨x, hx⟩ | hb) + · rcases H₂ hb hx with ⟨y, hya, hyb⟩ + exact infᵢ₂_le_of_le y hya (principal_mono.2 fun z hz => (hf.2 hz).trans_le hyb) + · push_neg at hb + exact le_principal_iff.2 (univ_mem' hb) + +theorem induced_orderTopology' {α : Type u} {β : Type v} [Preorder α] [ta : TopologicalSpace β] + [Preorder β] [OrderTopology β] (f : α → β) (hf : ∀ {x y}, f x < f y ↔ x < y) + (H₁ : ∀ {a x}, x < f a → ∃ b < a, x ≤ f b) (H₂ : ∀ {a x}, f a < x → ∃ b > a, f b ≤ x) : + @OrderTopology _ (induced f ta) _ := + let _ := induced f ta + ⟨induced_topology_eq_preorder hf (fun h _ => H₁ h) (fun h _ => H₂ h)⟩ +#align induced_order_topology' induced_orderTopology' + +theorem induced_orderTopology {α : Type u} {β : Type v} [Preorder α] [ta : TopologicalSpace β] + [Preorder β] [OrderTopology β] (f : α → β) (hf : ∀ {x y}, f x < f y ↔ x < y) + (H : ∀ {x y}, x < y → ∃ a, x < f a ∧ f a < y) : @OrderTopology _ (induced f ta) _ := + induced_orderTopology' f (hf) + (fun xa => let ⟨b, xb, ba⟩ := H xa; ⟨b, hf.1 ba, le_of_lt xb⟩) + fun ax => let ⟨b, ab, bx⟩ := H ax; ⟨b, hf.1 ab, le_of_lt bx⟩ +#align induced_order_topology induced_orderTopology + +/-- On an `Set.OrdConnected` subset of a linear order, the order topology for the restriction of the +order is the same as the restriction to the subset of the order topology. -/ +instance orderTopology_of_ordConnected {α : Type u} [TopologicalSpace α] [LinearOrder α] + [OrderTopology α] {t : Set α} [ht : OrdConnected t] : OrderTopology t := by + refine ⟨induced_topology_eq_preorder Iff.rfl (fun h₁ h₂ => ?_) (fun h₁ h₂ => ?_)⟩ + · have := ht.out (Subtype.property _) (Subtype.property _) ⟨not_lt.1 h₂, h₁.le⟩ + exact ⟨⟨_, this⟩, h₁, le_rfl⟩ + · have := ht.out (Subtype.property _) (Subtype.property _) ⟨h₁.le, not_lt.1 h₂⟩ + exact ⟨⟨_, this⟩, h₁, le_rfl⟩ +#align order_topology_of_ord_connected orderTopology_of_ordConnected + +theorem nhdsWithin_Ici_eq'' [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) : + 𝓝[≥] a = (⨅ (u) (_hu : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a) := by + rw [nhdsWithin, nhds_eq_order] + refine' le_antisymm (inf_le_inf_right _ inf_le_right) (le_inf (le_inf _ inf_le_left) inf_le_right) + exact inf_le_right.trans (le_infᵢ₂ fun l hl => principal_mono.2 <| Ici_subset_Ioi.2 hl) +#align nhds_within_Ici_eq'' nhdsWithin_Ici_eq'' + +theorem nhdsWithin_Iic_eq'' [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) : + 𝓝[≤] a = (⨅ l < a, 𝓟 (Ioi l)) ⊓ 𝓟 (Iic a) := + nhdsWithin_Ici_eq'' (toDual a) +#align nhds_within_Iic_eq'' nhdsWithin_Iic_eq'' + +theorem nhdsWithin_Ici_eq' [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} + (ha : ∃ u, a < u) : 𝓝[≥] a = ⨅ (u) (_hu : a < u), 𝓟 (Ico a u) := by + simp only [nhdsWithin_Ici_eq'', binfᵢ_inf ha, inf_principal, Iio_inter_Ici] +#align nhds_within_Ici_eq' nhdsWithin_Ici_eq' + +theorem nhdsWithin_Iic_eq' [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} + (ha : ∃ l, l < a) : 𝓝[≤] a = ⨅ l < a, 𝓟 (Ioc l a) := by + simp only [nhdsWithin_Iic_eq'', binfᵢ_inf ha, inf_principal, Ioi_inter_Iic] +#align nhds_within_Iic_eq' nhdsWithin_Iic_eq' + +theorem nhdsWithin_Ici_basis' [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} + (ha : ∃ u, a < u) : (𝓝[≥] a).HasBasis (fun u => a < u) fun u => Ico a u := + (nhdsWithin_Ici_eq' ha).symm ▸ + hasBasis_binfᵢ_principal + (fun b hb c hc => ⟨min b c, lt_min hb hc, Ico_subset_Ico_right (min_le_left _ _), + Ico_subset_Ico_right (min_le_right _ _)⟩) + ha +#align nhds_within_Ici_basis' nhdsWithin_Ici_basis' + +theorem nhdsWithin_Iic_basis' [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} + (ha : ∃ l, l < a) : (𝓝[≤] a).HasBasis (fun l => l < a) fun l => Ioc l a := by + convert @nhdsWithin_Ici_basis' αᵒᵈ _ _ _ (toDual a) ha + exact funext fun x => (@dual_Ico _ _ _ _).symm +#align nhds_within_Iic_basis' nhdsWithin_Iic_basis' + +theorem nhdsWithin_Ici_basis [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] + (a : α) : (𝓝[≥] a).HasBasis (fun u => a < u) fun u => Ico a u := + nhdsWithin_Ici_basis' (exists_gt a) +#align nhds_within_Ici_basis nhdsWithin_Ici_basis + +theorem nhdsWithin_Iic_basis [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] + (a : α) : (𝓝[≤] a).HasBasis (fun l => l < a) fun l => Ioc l a := + nhdsWithin_Iic_basis' (exists_lt a) +#align nhds_within_Iic_basis nhdsWithin_Iic_basis + +theorem nhds_top_order [TopologicalSpace α] [Preorder α] [OrderTop α] [OrderTopology α] : + 𝓝 (⊤ : α) = ⨅ (l) (h₂ : l < ⊤), 𝓟 (Ioi l) := by simp [nhds_eq_order (⊤ : α)] +#align nhds_top_order nhds_top_order + +theorem nhds_bot_order [TopologicalSpace α] [Preorder α] [OrderBot α] [OrderTopology α] : + 𝓝 (⊥ : α) = ⨅ (l) (h₂ : ⊥ < l), 𝓟 (Iio l) := by simp [nhds_eq_order (⊥ : α)] +#align nhds_bot_order nhds_bot_order + +theorem nhds_top_basis [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α] + [Nontrivial α] : (𝓝 ⊤).HasBasis (fun a : α => a < ⊤) fun a : α => Ioi a := by + have : ∃ x : α, x < ⊤ := (exists_ne ⊤).imp fun x hx => hx.lt_top + simpa only [Iic_top, nhdsWithin_univ, Ioc_top] using nhdsWithin_Iic_basis' this +#align nhds_top_basis nhds_top_basis + +theorem nhds_bot_basis [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α] + [Nontrivial α] : (𝓝 ⊥).HasBasis (fun a : α => ⊥ < a) fun a : α => Iio a := + @nhds_top_basis αᵒᵈ _ _ _ _ _ +#align nhds_bot_basis nhds_bot_basis + +theorem nhds_top_basis_Ici [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α] + [Nontrivial α] [DenselyOrdered α] : (𝓝 ⊤).HasBasis (fun a : α => a < ⊤) Ici := + nhds_top_basis.to_hasBasis + (fun _a ha => let ⟨b, hab, hb⟩ := exists_between ha; ⟨b, hb, Ici_subset_Ioi.mpr hab⟩) + fun a ha => ⟨a, ha, Ioi_subset_Ici_self⟩ +#align nhds_top_basis_Ici nhds_top_basis_Ici + +theorem nhds_bot_basis_Iic [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α] + [Nontrivial α] [DenselyOrdered α] : (𝓝 ⊥).HasBasis (fun a : α => ⊥ < a) Iic := + @nhds_top_basis_Ici αᵒᵈ _ _ _ _ _ _ +#align nhds_bot_basis_Iic nhds_bot_basis_Iic + +theorem tendsto_nhds_top_mono [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β] + {l : Filter α} {f g : α → β} (hf : Tendsto f l (𝓝 ⊤)) (hg : f ≤ᶠ[l] g) : Tendsto g l (𝓝 ⊤) := by + simp only [nhds_top_order, tendsto_infᵢ, tendsto_principal] at hf ⊢ + intro x hx + filter_upwards [hf x hx, hg] with _ using lt_of_lt_of_le +#align tendsto_nhds_top_mono tendsto_nhds_top_mono + +theorem tendsto_nhds_bot_mono [TopologicalSpace β] [Preorder β] [OrderBot β] [OrderTopology β] + {l : Filter α} {f g : α → β} (hf : Tendsto f l (𝓝 ⊥)) (hg : g ≤ᶠ[l] f) : Tendsto g l (𝓝 ⊥) := + @tendsto_nhds_top_mono α βᵒᵈ _ _ _ _ _ _ _ hf hg +#align tendsto_nhds_bot_mono tendsto_nhds_bot_mono + +theorem tendsto_nhds_top_mono' [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β] + {l : Filter α} {f g : α → β} (hf : Tendsto f l (𝓝 ⊤)) (hg : f ≤ g) : Tendsto g l (𝓝 ⊤) := + tendsto_nhds_top_mono hf (eventually_of_forall hg) +#align tendsto_nhds_top_mono' tendsto_nhds_top_mono' + +theorem tendsto_nhds_bot_mono' [TopologicalSpace β] [Preorder β] [OrderBot β] [OrderTopology β] + {l : Filter α} {f g : α → β} (hf : Tendsto f l (𝓝 ⊥)) (hg : g ≤ f) : Tendsto g l (𝓝 ⊥) := + tendsto_nhds_bot_mono hf (eventually_of_forall hg) +#align tendsto_nhds_bot_mono' tendsto_nhds_bot_mono' + +section LinearOrder + +variable [TopologicalSpace α] [LinearOrder α] + +section OrderClosedTopology + +variable [OrderClosedTopology α] {a b : α} + +theorem eventually_le_nhds (hab : a < b) : ∀ᶠ x in 𝓝 a, x ≤ b := Iic_mem_nhds hab +#align eventually_le_nhds eventually_le_nhds + +theorem eventually_lt_nhds (hab : a < b) : ∀ᶠ x in 𝓝 a, x < b := Iio_mem_nhds hab +#align eventually_lt_nhds eventually_lt_nhds + +theorem eventually_ge_nhds (hab : b < a) : ∀ᶠ x in 𝓝 a, b ≤ x := Ici_mem_nhds hab +#align eventually_ge_nhds eventually_ge_nhds + +theorem eventually_gt_nhds (hab : b < a) : ∀ᶠ x in 𝓝 a, b < x := Ioi_mem_nhds hab +#align eventually_gt_nhds eventually_gt_nhds + +end OrderClosedTopology + +section OrderTopology + +variable [OrderTopology α] + +theorem order_separated {a₁ a₂ : α} (h : a₁ < a₂) : + ∃ u v : Set α, IsOpen u ∧ IsOpen v ∧ a₁ ∈ u ∧ a₂ ∈ v ∧ ∀ b₁ ∈ u, ∀ b₂ ∈ v, b₁ < b₂ := + let ⟨x, hx, y, hy, h⟩ := h.exists_disjoint_Iio_Ioi + ⟨Iio x, Ioi y, isOpen_gt' _, isOpen_lt' _, hx, hy, h⟩ +#align order_separated order_separated + +-- see Note [lower instance priority] +instance (priority := 100) OrderTopology.to_orderClosedTopology : OrderClosedTopology α where + isClosed_le' := isOpen_compl_iff.1 <| isOpen_prod_iff.mpr fun a₁ a₂ (h : ¬a₁ ≤ a₂) => + have h : a₂ < a₁ := lt_of_not_ge h + let ⟨u, v, hu, hv, ha₁, ha₂, h⟩ := order_separated h + ⟨v, u, hv, hu, ha₂, ha₁, fun ⟨b₁, b₂⟩ ⟨h₁, h₂⟩ => not_le_of_gt <| h b₂ h₂ b₁ h₁⟩ +#align order_topology.to_order_closed_topology OrderTopology.to_orderClosedTopology + +theorem exists_Ioc_subset_of_mem_nhds {a : α} {s : Set α} (hs : s ∈ 𝓝 a) (h : ∃ l, l < a) : + ∃ l < a, Ioc l a ⊆ s := + (nhdsWithin_Iic_basis' h).mem_iff.mp (nhdsWithin_le_nhds hs) +#align exists_Ioc_subset_of_mem_nhds exists_Ioc_subset_of_mem_nhds + +theorem exists_Ioc_subset_of_mem_nhds' {a : α} {s : Set α} (hs : s ∈ 𝓝 a) {l : α} (hl : l < a) : + ∃ l' ∈ Ico l a, Ioc l' a ⊆ s := + let ⟨l', hl'a, hl's⟩ := exists_Ioc_subset_of_mem_nhds hs ⟨l, hl⟩ + ⟨max l l', ⟨le_max_left _ _, max_lt hl hl'a⟩, + (Ioc_subset_Ioc_left <| le_max_right _ _).trans hl's⟩ +#align exists_Ioc_subset_of_mem_nhds' exists_Ioc_subset_of_mem_nhds' + +theorem exists_Ico_subset_of_mem_nhds' {a : α} {s : Set α} (hs : s ∈ 𝓝 a) {u : α} (hu : a < u) : + ∃ u' ∈ Ioc a u, Ico a u' ⊆ s := by + simpa only [OrderDual.exists, exists_prop, dual_Ico, dual_Ioc] using + exists_Ioc_subset_of_mem_nhds' (show ofDual ⁻¹' s ∈ 𝓝 (toDual a) from hs) hu.dual +#align exists_Ico_subset_of_mem_nhds' exists_Ico_subset_of_mem_nhds' + +theorem exists_Ico_subset_of_mem_nhds {a : α} {s : Set α} (hs : s ∈ 𝓝 a) (h : ∃ u, a < u) : + ∃ u, a < u ∧ Ico a u ⊆ s := + let ⟨_l', hl'⟩ := h; + let ⟨l, hl⟩ := exists_Ico_subset_of_mem_nhds' hs hl' + ⟨l, hl.1.1, hl.2⟩ +#align exists_Ico_subset_of_mem_nhds exists_Ico_subset_of_mem_nhds + +theorem exists_Icc_mem_subset_of_mem_nhdsWithin_Ici {a : α} {s : Set α} (hs : s ∈ 𝓝[≥] a) : + ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s := by + rcases (em (IsMax a)).imp_right not_isMax_iff.mp with (ha | ha) + · use a + simpa [ha.Ici_eq] using hs + · rcases(nhdsWithin_Ici_basis' ha).mem_iff.mp hs with ⟨b, hab, hbs⟩ + rcases eq_empty_or_nonempty (Ioo a b) with (H | ⟨c, hac, hcb⟩) + · have : Ico a b = Icc a a := by rw [← Icc_union_Ioo_eq_Ico le_rfl hab, H, union_empty] + exact ⟨a, le_rfl, this ▸ ⟨Ico_mem_nhdsWithin_Ici' hab, hbs⟩⟩ + · refine' ⟨c, hac.le, Icc_mem_nhdsWithin_Ici' hac, _⟩ + exact (Icc_subset_Ico_right hcb).trans hbs +#align exists_Icc_mem_subset_of_mem_nhds_within_Ici exists_Icc_mem_subset_of_mem_nhdsWithin_Ici + +theorem exists_Icc_mem_subset_of_mem_nhdsWithin_Iic {a : α} {s : Set α} (hs : s ∈ 𝓝[≤] a) : + ∃ b ≤ a, Icc b a ∈ 𝓝[≤] a ∧ Icc b a ⊆ s := by + simpa only [dual_Icc, toDual.surjective.exists] using + @exists_Icc_mem_subset_of_mem_nhdsWithin_Ici αᵒᵈ _ _ _ (toDual a) _ hs +#align exists_Icc_mem_subset_of_mem_nhds_within_Iic exists_Icc_mem_subset_of_mem_nhdsWithin_Iic + +theorem exists_Icc_mem_subset_of_mem_nhds {a : α} {s : Set α} (hs : s ∈ 𝓝 a) : + ∃ b c, a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s := by + rcases exists_Icc_mem_subset_of_mem_nhdsWithin_Iic (nhdsWithin_le_nhds hs) with + ⟨b, hba, hb_nhds, hbs⟩ + rcases exists_Icc_mem_subset_of_mem_nhdsWithin_Ici (nhdsWithin_le_nhds hs) with + ⟨c, hac, hc_nhds, hcs⟩ + refine' ⟨b, c, ⟨hba, hac⟩, _⟩ + rw [← Icc_union_Icc_eq_Icc hba hac, ← nhds_left_sup_nhds_right] + exact ⟨union_mem_sup hb_nhds hc_nhds, union_subset hbs hcs⟩ +#align exists_Icc_mem_subset_of_mem_nhds exists_Icc_mem_subset_of_mem_nhds + +theorem IsOpen.exists_Ioo_subset [Nontrivial α] {s : Set α} (hs : IsOpen s) (h : s.Nonempty) : + ∃ a b, a < b ∧ Ioo a b ⊆ s := by + obtain ⟨x, hx⟩ : ∃ x, x ∈ s := h + obtain ⟨y, hy⟩ : ∃ y, y ≠ x := exists_ne x + rcases lt_trichotomy x y with (H | rfl | H) + · obtain ⟨u, xu, hu⟩ : ∃ u, x < u ∧ Ico x u ⊆ s := + exists_Ico_subset_of_mem_nhds (hs.mem_nhds hx) ⟨y, H⟩ + exact ⟨x, u, xu, Ioo_subset_Ico_self.trans hu⟩ + · exact (hy rfl).elim + · obtain ⟨l, lx, hl⟩ : ∃ l, l < x ∧ Ioc l x ⊆ s := + exists_Ioc_subset_of_mem_nhds (hs.mem_nhds hx) ⟨y, H⟩ + exact ⟨l, x, lx, Ioo_subset_Ioc_self.trans hl⟩ +#align is_open.exists_Ioo_subset IsOpen.exists_Ioo_subset + +theorem dense_of_exists_between [Nontrivial α] {s : Set α} + (h : ∀ ⦃a b⦄, a < b → ∃ c ∈ s, a < c ∧ c < b) : Dense s := by + refine dense_iff_inter_open.2 fun U U_open U_nonempty => ?_ + obtain ⟨a, b, hab, H⟩ : ∃ a b : α, a < b ∧ Ioo a b ⊆ U := U_open.exists_Ioo_subset U_nonempty + obtain ⟨x, xs, hx⟩ : ∃ x ∈ s, a < x ∧ x < b := h hab + exact ⟨x, ⟨H hx, xs⟩⟩ +#align dense_of_exists_between dense_of_exists_between + +/-- A set in a nontrivial densely linear ordered type is dense in the sense of topology if and only +if for any `a < b` there exists `c ∈ s`, `a < c < b`. Each implication requires less typeclass +assumptions. -/ +theorem dense_iff_exists_between [DenselyOrdered α] [Nontrivial α] {s : Set α} : + Dense s ↔ ∀ a b, a < b → ∃ c ∈ s, a < c ∧ c < b := + ⟨fun h _ _ hab => h.exists_between hab, dense_of_exists_between⟩ +#align dense_iff_exists_between dense_iff_exists_between + +/-- A set is a neighborhood of `a` if and only if it contains an interval `(l, u)` containing `a`, +provided `a` is neither a bottom element nor a top element. -/ +theorem mem_nhds_iff_exists_Ioo_subset' {a : α} {s : Set α} (hl : ∃ l, l < a) (hu : ∃ u, a < u) : + s ∈ 𝓝 a ↔ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s := by + constructor + · intro h + rcases exists_Ico_subset_of_mem_nhds h hu with ⟨u, au, hu⟩ + rcases exists_Ioc_subset_of_mem_nhds h hl with ⟨l, la, hl⟩ + exact ⟨l, u, ⟨la, au⟩, Ioc_union_Ico_eq_Ioo la au ▸ union_subset hl hu⟩ + · rintro ⟨l, u, ha, h⟩ + apply mem_of_superset (Ioo_mem_nhds ha.1 ha.2) h +#align mem_nhds_iff_exists_Ioo_subset' mem_nhds_iff_exists_Ioo_subset' + +/-- A set is a neighborhood of `a` if and only if it contains an interval `(l, u)` containing `a`. +-/ +theorem mem_nhds_iff_exists_Ioo_subset [NoMaxOrder α] [NoMinOrder α] {a : α} {s : Set α} : + s ∈ 𝓝 a ↔ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s := + mem_nhds_iff_exists_Ioo_subset' (exists_lt a) (exists_gt a) +#align mem_nhds_iff_exists_Ioo_subset mem_nhds_iff_exists_Ioo_subset + +theorem nhds_basis_Ioo' {a : α} (hl : ∃ l, l < a) (hu : ∃ u, a < u) : + (𝓝 a).HasBasis (fun b : α × α => b.1 < a ∧ a < b.2) fun b => Ioo b.1 b.2 := + ⟨fun s => (mem_nhds_iff_exists_Ioo_subset' hl hu).trans <| by simp⟩ +#align nhds_basis_Ioo' nhds_basis_Ioo' + +theorem nhds_basis_Ioo [NoMaxOrder α] [NoMinOrder α] (a : α) : + (𝓝 a).HasBasis (fun b : α × α => b.1 < a ∧ a < b.2) fun b => Ioo b.1 b.2 := + nhds_basis_Ioo' (exists_lt a) (exists_gt a) +#align nhds_basis_Ioo nhds_basis_Ioo + +theorem Filter.Eventually.exists_Ioo_subset [NoMaxOrder α] [NoMinOrder α] {a : α} {p : α → Prop} + (hp : ∀ᶠ x in 𝓝 a, p x) : ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ { x | p x } := + mem_nhds_iff_exists_Ioo_subset.1 hp +#align filter.eventually.exists_Ioo_subset Filter.Eventually.exists_Ioo_subset + +-- porting note: new lemma +/-- The set of points which are isolated on the right is countable when the space is +second-countable. -/ +theorem countable_setOf_covby_right [SecondCountableTopology α] : + Set.Countable { x : α | ∃ y, x ⋖ y } := by + nontriviality α + let s := { x : α | ∃ y, x ⋖ y } + have : ∀ x ∈ s, ∃ y, x ⋖ y := fun x => id + choose! y hy using this + have Hy : ∀ x z, x ∈ s → z < y x → z ≤ x := fun x z hx => (hy x hx).le_of_lt + suffices H : ∀ a : Set α, IsOpen a → Set.Countable { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a } + · have : s ⊆ ⋃ a ∈ countableBasis α, { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a } := fun x hx => by + rcases (isBasis_countableBasis α).exists_mem_of_ne (hy x hx).ne with ⟨a, ab, xa, ya⟩ + exact mem_unionᵢ₂.2 ⟨a, ab, hx, xa, ya⟩ + refine Set.Countable.mono this ?_ + refine' Countable.bunionᵢ (countable_countableBasis α) fun a ha => H _ _ + exact isOpen_of_mem_countableBasis ha + intro a ha + suffices H : Set.Countable { x | (x ∈ s ∧ x ∈ a ∧ y x ∉ a) ∧ ¬IsBot x } + · exact H.of_diff (subsingleton_isBot α).countable + simp only [and_assoc] + let t := { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x } + have : ∀ x ∈ t, ∃ z < x, Ioc z x ⊆ a := by + intro x hx + apply exists_Ioc_subset_of_mem_nhds (ha.mem_nhds hx.2.1) + simpa only [IsBot, not_forall, not_le] using hx.right.right.right + choose! z hz h'z using this + have : PairwiseDisjoint t fun x => Ioc (z x) x := fun x xt x' x't hxx' => by + rcases hxx'.lt_or_lt with (h' | h') + · refine' disjoint_left.2 fun u ux ux' => xt.2.2.1 _ + refine' h'z x' x't ⟨ux'.1.trans_le (ux.2.trans (hy x xt.1).le), _⟩ + by_contra' H + exact False.elim (lt_irrefl _ ((Hy _ _ xt.1 H).trans_lt h')) + · refine' disjoint_left.2 fun u ux ux' => x't.2.2.1 _ + refine' h'z x xt ⟨ux.1.trans_le (ux'.2.trans (hy x' x't.1).le), _⟩ + by_contra' H + exact False.elim (lt_irrefl _ ((Hy _ _ x't.1 H).trans_lt h')) + refine' this.countable_of_isOpen (fun x hx => _) fun x hx => ⟨x, hz x hx, le_rfl⟩ + suffices H : Ioc (z x) x = Ioo (z x) (y x) + · rw [H] + exact isOpen_Ioo + exact Subset.antisymm (Ioc_subset_Ioo_right (hy x hx.1).lt) fun u hu => ⟨hu.1, Hy _ _ hx.1 hu.2⟩ + +/-- The set of points which are isolated on the right is countable when the space is +second-countable. -/ +@[deprecated countable_setOf_covby_right] +theorem countable_of_isolated_right' [SecondCountableTopology α] : + Set.Countable { x : α | ∃ y, x < y ∧ Ioo x y = ∅ } := by + simpa only [← covby_iff_Ioo_eq] using countable_setOf_covby_right +#align countable_of_isolated_right countable_of_isolated_right' + +/-- The set of points which are isolated on the left is countable when the space is +second-countable. -/ +theorem countable_setOf_covby_left [SecondCountableTopology α] : + Set.Countable { x : α | ∃ y, y ⋖ x } := by + convert @countable_setOf_covby_right αᵒᵈ _ _ _ _ + exact Set.ext fun x => exists_congr fun y => toDual_covby_toDual_iff.symm + +/-- The set of points which are isolated on the left is countable when the space is +second-countable. -/ +theorem countable_of_isolated_left' [SecondCountableTopology α] : + Set.Countable { x : α | ∃ y, y < x ∧ Ioo y x = ∅ } := by + simpa only [← covby_iff_Ioo_eq] using countable_setOf_covby_left +#align countable_of_isolated_left countable_of_isolated_left' + +/-- Consider a disjoint family of intervals `(x, y)` with `x < y` in a second-countable space. +Then the family is countable. +This is not a straightforward consequence of second-countability as some of these intervals might be +empty (but in fact this can happen only for countably many of them). -/ +theorem Set.PairwiseDisjoint.countable_of_Ioo [SecondCountableTopology α] {y : α → α} {s : Set α} + (h : PairwiseDisjoint s fun x => Ioo x (y x)) (h' : ∀ x ∈ s, x < y x) : s.Countable := + have : (s \ { x | ∃ y, x ⋖ y }).Countable := + (h.subset (diff_subset _ _)).countable_of_isOpen (fun _ _ => isOpen_Ioo) + fun x hx => (h' _ hx.1).exists_lt_lt (mt (Exists.intro (y x)) hx.2) + this.of_diff countable_setOf_covby_right +#align set.pairwise_disjoint.countable_of_Ioo Set.PairwiseDisjoint.countable_of_Ioo + +section Pi + +/-! +### Intervals in `Π i, π i` belong to `𝓝 x` + +For each lemma `pi_Ixx_mem_nhds` we add a non-dependent version `pi_Ixx_mem_nhds'` because +sometimes Lean fails to unify different instances while trying to apply the dependent version to, +e.g., `ι → ℝ`. +-/ + +variable {ι : Type _} {π : ι → Type _} [Finite ι] [∀ i, LinearOrder (π i)] + [∀ i, TopologicalSpace (π i)] [∀ i, OrderTopology (π i)] {a b x : ∀ i, π i} {a' b' x' : ι → α} + +theorem pi_Iic_mem_nhds (ha : ∀ i, x i < a i) : Iic a ∈ 𝓝 x := + pi_univ_Iic a ▸ set_pi_mem_nhds (Set.toFinite _) fun _ _ => Iic_mem_nhds (ha _) +#align pi_Iic_mem_nhds pi_Iic_mem_nhds + +theorem pi_Iic_mem_nhds' (ha : ∀ i, x' i < a' i) : Iic a' ∈ 𝓝 x' := + pi_Iic_mem_nhds ha +#align pi_Iic_mem_nhds' pi_Iic_mem_nhds' + +theorem pi_Ici_mem_nhds (ha : ∀ i, a i < x i) : Ici a ∈ 𝓝 x := + pi_univ_Ici a ▸ set_pi_mem_nhds (Set.toFinite _) fun _ _ => Ici_mem_nhds (ha _) +#align pi_Ici_mem_nhds pi_Ici_mem_nhds + +theorem pi_Ici_mem_nhds' (ha : ∀ i, a' i < x' i) : Ici a' ∈ 𝓝 x' := + pi_Ici_mem_nhds ha +#align pi_Ici_mem_nhds' pi_Ici_mem_nhds' + +theorem pi_Icc_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Icc a b ∈ 𝓝 x := + pi_univ_Icc a b ▸ set_pi_mem_nhds finite_univ fun _ _ => Icc_mem_nhds (ha _) (hb _) +#align pi_Icc_mem_nhds pi_Icc_mem_nhds + +theorem pi_Icc_mem_nhds' (ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : Icc a' b' ∈ 𝓝 x' := + pi_Icc_mem_nhds ha hb +#align pi_Icc_mem_nhds' pi_Icc_mem_nhds' + +variable [Nonempty ι] + +theorem pi_Iio_mem_nhds (ha : ∀ i, x i < a i) : Iio a ∈ 𝓝 x := by + refine' mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => _) (pi_univ_Iio_subset a) + exact Iio_mem_nhds (ha i) +#align pi_Iio_mem_nhds pi_Iio_mem_nhds + +theorem pi_Iio_mem_nhds' (ha : ∀ i, x' i < a' i) : Iio a' ∈ 𝓝 x' := + pi_Iio_mem_nhds ha +#align pi_Iio_mem_nhds' pi_Iio_mem_nhds' + +theorem pi_Ioi_mem_nhds (ha : ∀ i, a i < x i) : Ioi a ∈ 𝓝 x := + @pi_Iio_mem_nhds ι (fun i => (π i)ᵒᵈ) _ _ _ _ _ _ _ ha +#align pi_Ioi_mem_nhds pi_Ioi_mem_nhds + +theorem pi_Ioi_mem_nhds' (ha : ∀ i, a' i < x' i) : Ioi a' ∈ 𝓝 x' := + pi_Ioi_mem_nhds ha +#align pi_Ioi_mem_nhds' pi_Ioi_mem_nhds' + +theorem pi_Ioc_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Ioc a b ∈ 𝓝 x := by + refine' mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => _) (pi_univ_Ioc_subset a b) + exact Ioc_mem_nhds (ha i) (hb i) +#align pi_Ioc_mem_nhds pi_Ioc_mem_nhds + +theorem pi_Ioc_mem_nhds' (ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : Ioc a' b' ∈ 𝓝 x' := + pi_Ioc_mem_nhds ha hb +#align pi_Ioc_mem_nhds' pi_Ioc_mem_nhds' + +theorem pi_Ico_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Ico a b ∈ 𝓝 x := by + refine' mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => _) (pi_univ_Ico_subset a b) + exact Ico_mem_nhds (ha i) (hb i) +#align pi_Ico_mem_nhds pi_Ico_mem_nhds + +theorem pi_Ico_mem_nhds' (ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : Ico a' b' ∈ 𝓝 x' := + pi_Ico_mem_nhds ha hb +#align pi_Ico_mem_nhds' pi_Ico_mem_nhds' + +theorem pi_Ioo_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Ioo a b ∈ 𝓝 x := by + refine' mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => _) (pi_univ_Ioo_subset a b) + exact Ioo_mem_nhds (ha i) (hb i) +#align pi_Ioo_mem_nhds pi_Ioo_mem_nhds + +theorem pi_Ioo_mem_nhds' (ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : Ioo a' b' ∈ 𝓝 x' := + pi_Ioo_mem_nhds ha hb +#align pi_Ioo_mem_nhds' pi_Ioo_mem_nhds' + +end Pi + +theorem disjoint_nhds_atTop [NoMaxOrder α] (x : α) : Disjoint (𝓝 x) atTop := by + rcases exists_gt x with ⟨y, hy : x < y⟩ + refine' disjoint_of_disjoint_of_mem _ (Iio_mem_nhds hy) (mem_atTop y) + exact disjoint_left.mpr fun z => not_le.2 +#align disjoint_nhds_at_top disjoint_nhds_atTop + +@[simp] +theorem inf_nhds_atTop [NoMaxOrder α] (x : α) : 𝓝 x ⊓ atTop = ⊥ := + disjoint_iff.1 (disjoint_nhds_atTop x) +#align inf_nhds_at_top inf_nhds_atTop + +theorem disjoint_nhds_atBot [NoMinOrder α] (x : α) : Disjoint (𝓝 x) atBot := + @disjoint_nhds_atTop αᵒᵈ _ _ _ _ x +#align disjoint_nhds_at_bot disjoint_nhds_atBot + +@[simp] +theorem inf_nhds_atBot [NoMinOrder α] (x : α) : 𝓝 x ⊓ atBot = ⊥ := + @inf_nhds_atTop αᵒᵈ _ _ _ _ x +#align inf_nhds_at_bot inf_nhds_atBot + +theorem not_tendsto_nhds_of_tendsto_atTop [NoMaxOrder α] {F : Filter β} [NeBot F] {f : β → α} + (hf : Tendsto f F atTop) (x : α) : ¬Tendsto f F (𝓝 x) := + hf.not_tendsto (disjoint_nhds_atTop x).symm +#align not_tendsto_nhds_of_tendsto_at_top not_tendsto_nhds_of_tendsto_atTop + +theorem not_tendsto_atTop_of_tendsto_nhds [NoMaxOrder α] {F : Filter β} [NeBot F] {f : β → α} + {x : α} (hf : Tendsto f F (𝓝 x)) : ¬Tendsto f F atTop := + hf.not_tendsto (disjoint_nhds_atTop x) +#align not_tendsto_at_top_of_tendsto_nhds not_tendsto_atTop_of_tendsto_nhds + +theorem not_tendsto_nhds_of_tendsto_atBot [NoMinOrder α] {F : Filter β} [NeBot F] {f : β → α} + (hf : Tendsto f F atBot) (x : α) : ¬Tendsto f F (𝓝 x) := + hf.not_tendsto (disjoint_nhds_atBot x).symm +#align not_tendsto_nhds_of_tendsto_at_bot not_tendsto_nhds_of_tendsto_atBot + +theorem not_tendsto_atBot_of_tendsto_nhds [NoMinOrder α] {F : Filter β} [NeBot F] {f : β → α} + {x : α} (hf : Tendsto f F (𝓝 x)) : ¬Tendsto f F atBot := + hf.not_tendsto (disjoint_nhds_atBot x) +#align not_tendsto_at_bot_of_tendsto_nhds not_tendsto_atBot_of_tendsto_nhds + +/-! +### Neighborhoods to the left and to the right on an `OrderTopology` + +We've seen some properties of left and right neighborhood of a point in an `OrderClosedTopology`. +In an `OrderTopology`, such neighborhoods can be characterized as the sets containing suitable +intervals to the right or to the left of `a`. We give now these characterizations. -/ + +open List in +/-- The following statements are equivalent: + +0. `s` is a neighborhood of `a` within `(a, +∞)`; +1. `s` is a neighborhood of `a` within `(a, b]`; +2. `s` is a neighborhood of `a` within `(a, b)`; +3. `s` includes `(a, u)` for some `u ∈ (a, b]`; +4. `s` includes `(a, u)` for some `u > a`. +-/ +theorem TFAE_mem_nhdsWithin_Ioi {a b : α} (hab : a < b) (s : Set α) : + TFAE [s ∈ 𝓝[>] a, + s ∈ 𝓝[Ioc a b] a, + s ∈ 𝓝[Ioo a b] a, + ∃ u ∈ Ioc a b, Ioo a u ⊆ s, + ∃ u ∈ Ioi a, Ioo a u ⊆ s] := by + rw [nhdsWithin_Ioc_eq_nhdsWithin_Ioi hab, nhdsWithin_Ioo_eq_nhdsWithin_Ioi hab] + apply_rules [tfae_of_cycle, Chain.cons, Chain.nil] <;> try { exact id } + · rw [nhdsWithin, mem_inf_principal] + intro h + rcases exists_Ico_subset_of_mem_nhds' h hab with ⟨u, au, hu⟩ + exact ⟨u, au, fun x hx => hu (Ioo_subset_Ico_self hx) hx.1⟩ + · rintro ⟨u, hu, hs⟩ + exact ⟨u, hu.1, hs⟩ + · rintro ⟨u, hu, hs⟩ + exact mem_of_superset (Ioo_mem_nhdsWithin_Ioi' hu) hs +#align tfae_mem_nhds_within_Ioi TFAE_mem_nhdsWithin_Ioi + +theorem mem_nhdsWithin_Ioi_iff_exists_mem_Ioc_Ioo_subset {a u' : α} {s : Set α} (hu' : a < u') : + s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioc a u', Ioo a u ⊆ s := + (TFAE_mem_nhdsWithin_Ioi hu' s).out 0 3 +#align mem_nhds_within_Ioi_iff_exists_mem_Ioc_Ioo_subset mem_nhdsWithin_Ioi_iff_exists_mem_Ioc_Ioo_subset + +/-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u)` +with `a < u < u'`, provided `a` is not a top element. -/ +theorem mem_nhdsWithin_Ioi_iff_exists_Ioo_subset' {a u' : α} {s : Set α} (hu' : a < u') : + s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioo a u ⊆ s := + (TFAE_mem_nhdsWithin_Ioi hu' s).out 0 4 +#align mem_nhds_within_Ioi_iff_exists_Ioo_subset' mem_nhdsWithin_Ioi_iff_exists_Ioo_subset' + +/-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u)` +with `a < u`. -/ +theorem mem_nhdsWithin_Ioi_iff_exists_Ioo_subset [NoMaxOrder α] {a : α} {s : Set α} : + s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioo a u ⊆ s := + let ⟨_u', hu'⟩ := exists_gt a + mem_nhdsWithin_Ioi_iff_exists_Ioo_subset' hu' +#align mem_nhds_within_Ioi_iff_exists_Ioo_subset mem_nhdsWithin_Ioi_iff_exists_Ioo_subset + +/-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u]` +with `a < u`. -/ +theorem mem_nhdsWithin_Ioi_iff_exists_Ioc_subset [NoMaxOrder α] [DenselyOrdered α] {a : α} + {s : Set α} : s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s := by + rw [mem_nhdsWithin_Ioi_iff_exists_Ioo_subset] + constructor + · rintro ⟨u, au, as⟩ + rcases exists_between au with ⟨v, hv⟩ + exact ⟨v, hv.1, fun x hx => as ⟨hx.1, lt_of_le_of_lt hx.2 hv.2⟩⟩ + · rintro ⟨u, au, as⟩ + exact ⟨u, au, Subset.trans Ioo_subset_Ioc_self as⟩ +#align mem_nhds_within_Ioi_iff_exists_Ioc_subset mem_nhdsWithin_Ioi_iff_exists_Ioc_subset + +open List in +/-- The following statements are equivalent: + +0. `s` is a neighborhood of `b` within `(-∞, b)` +1. `s` is a neighborhood of `b` within `[a, b)` +2. `s` is a neighborhood of `b` within `(a, b)` +3. `s` includes `(l, b)` for some `l ∈ [a, b)` +4. `s` includes `(l, b)` for some `l < b` -/ +theorem TFAE_mem_nhdsWithin_Iio {a b : α} (h : a < b) (s : Set α) : + TFAE [s ∈ 𝓝[<] b,-- 0 : `s` is a neighborhood of `b` within `(-∞, b)` + s ∈ 𝓝[Ico a b] b,-- 1 : `s` is a neighborhood of `b` within `[a, b)` + s ∈ 𝓝[Ioo a b] b,-- 2 : `s` is a neighborhood of `b` within `(a, b)` + ∃ l ∈ Ico a b, Ioo l b ⊆ s,-- 3 : `s` includes `(l, b)` for some `l ∈ [a, b)` + ∃ l ∈ Iio b, Ioo l b ⊆ s] := by-- 4 : `s` includes `(l, b)` for some `l < b` + simpa only [exists_prop, OrderDual.exists, dual_Ioi, dual_Ioc, dual_Ioo] using + TFAE_mem_nhdsWithin_Ioi h.dual (ofDual ⁻¹' s) +#align tfae_mem_nhds_within_Iio TFAE_mem_nhdsWithin_Iio + +theorem mem_nhdsWithin_Iio_iff_exists_mem_Ico_Ioo_subset {a l' : α} {s : Set α} (hl' : l' < a) : + s ∈ 𝓝[<] a ↔ ∃ l ∈ Ico l' a, Ioo l a ⊆ s := + (TFAE_mem_nhdsWithin_Iio hl' s).out 0 3 +#align mem_nhds_within_Iio_iff_exists_mem_Ico_Ioo_subset mem_nhdsWithin_Iio_iff_exists_mem_Ico_Ioo_subset + +/-- A set is a neighborhood of `a` within `(-∞, a)` if and only if it contains an interval `(l, a)` +with `l < a`, provided `a` is not a bottom element. -/ +theorem mem_nhdsWithin_Iio_iff_exists_Ioo_subset' {a l' : α} {s : Set α} (hl' : l' < a) : + s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ioo l a ⊆ s := + (TFAE_mem_nhdsWithin_Iio hl' s).out 0 4 +#align mem_nhds_within_Iio_iff_exists_Ioo_subset' mem_nhdsWithin_Iio_iff_exists_Ioo_subset' + +/-- A set is a neighborhood of `a` within `(-∞, a)` if and only if it contains an interval `(l, a)` +with `l < a`. -/ +theorem mem_nhdsWithin_Iio_iff_exists_Ioo_subset [NoMinOrder α] {a : α} {s : Set α} : + s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ioo l a ⊆ s := + let ⟨_, h⟩ := exists_lt a + mem_nhdsWithin_Iio_iff_exists_Ioo_subset' h +#align mem_nhds_within_Iio_iff_exists_Ioo_subset mem_nhdsWithin_Iio_iff_exists_Ioo_subset + +/-- A set is a neighborhood of `a` within `(-∞, a)` if and only if it contains an interval `[l, a)` +with `l < a`. -/ +theorem mem_nhdsWithin_Iio_iff_exists_Ico_subset [NoMinOrder α] [DenselyOrdered α] {a : α} + {s : Set α} : s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ico l a ⊆ s := by + have : ofDual ⁻¹' s ∈ 𝓝[>] toDual a ↔ _ := mem_nhdsWithin_Ioi_iff_exists_Ioc_subset + simpa only [OrderDual.exists, exists_prop, dual_Ioc] using this +#align mem_nhds_within_Iio_iff_exists_Ico_subset mem_nhdsWithin_Iio_iff_exists_Ico_subset + +open List in +/-- The following statements are equivalent: + +0. `s` is a neighborhood of `a` within `[a, +∞)`; +1. `s` is a neighborhood of `a` within `[a, b]`; +2. `s` is a neighborhood of `a` within `[a, b)`; +3. `s` includes `[a, u)` for some `u ∈ (a, b]`; +4. `s` includes `[a, u)` for some `u > a`. +-/ +theorem TFAE_mem_nhdsWithin_Ici {a b : α} (hab : a < b) (s : Set α) : + TFAE [s ∈ 𝓝[≥] a, + s ∈ 𝓝[Icc a b] a, + s ∈ 𝓝[Ico a b] a, + ∃ u ∈ Ioc a b, Ico a u ⊆ s, + ∃ u ∈ Ioi a , Ico a u ⊆ s] := by + rw [nhdsWithin_Icc_eq_nhdsWithin_Ici hab, nhdsWithin_Ico_eq_nhdsWithin_Ici hab] + apply_rules [tfae_of_cycle, Chain.cons, Chain.nil] <;> try { exact id } + · rw [nhdsWithin, mem_inf_principal] + intro h + rcases exists_Ico_subset_of_mem_nhds' h hab with ⟨u, au, hu⟩ + exact ⟨u, au, fun x hx => hu hx hx.1⟩ + · rintro ⟨u, hu, hs⟩; exact ⟨u, hu.1, hs⟩ + · rintro ⟨u, hu, hs⟩; exact mem_of_superset (Ico_mem_nhdsWithin_Ici' hu) hs +#align tfae_mem_nhds_within_Ici TFAE_mem_nhdsWithin_Ici + +theorem mem_nhdsWithin_Ici_iff_exists_mem_Ioc_Ico_subset {a u' : α} {s : Set α} (hu' : a < u') : + s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioc a u', Ico a u ⊆ s := + (TFAE_mem_nhdsWithin_Ici hu' s).out 0 3 (by norm_num) (by norm_num) +#align mem_nhds_within_Ici_iff_exists_mem_Ioc_Ico_subset mem_nhdsWithin_Ici_iff_exists_mem_Ioc_Ico_subset + +/-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u)` +with `a < u < u'`, provided `a` is not a top element. -/ +theorem mem_nhdsWithin_Ici_iff_exists_Ico_subset' {a u' : α} {s : Set α} (hu' : a < u') : + s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s := + (TFAE_mem_nhdsWithin_Ici hu' s).out 0 4 (by norm_num) (by norm_num) +#align mem_nhds_within_Ici_iff_exists_Ico_subset' mem_nhdsWithin_Ici_iff_exists_Ico_subset' + +/-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u)` +with `a < u`. -/ +theorem mem_nhdsWithin_Ici_iff_exists_Ico_subset [NoMaxOrder α] {a : α} {s : Set α} : + s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s := + let ⟨_, hu'⟩ := exists_gt a + mem_nhdsWithin_Ici_iff_exists_Ico_subset' hu' +#align mem_nhds_within_Ici_iff_exists_Ico_subset mem_nhdsWithin_Ici_iff_exists_Ico_subset + +theorem nhdsWithin_Ici_basis_Ico [NoMaxOrder α] (a : α) : + (𝓝[≥] a).HasBasis (fun u => a < u) (Ico a) := + ⟨fun _ => mem_nhdsWithin_Ici_iff_exists_Ico_subset⟩ +#align nhds_within_Ici_basis_Ico nhdsWithin_Ici_basis_Ico + +/-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u]` +with `a < u`. -/ +theorem mem_nhdsWithin_Ici_iff_exists_Icc_subset [NoMaxOrder α] [DenselyOrdered α] {a : α} + {s : Set α} : s ∈ 𝓝[≥] a ↔ ∃ u, a < u ∧ Icc a u ⊆ s := by + rw [mem_nhdsWithin_Ici_iff_exists_Ico_subset] + constructor + · rintro ⟨u, au, as⟩ + rcases exists_between au with ⟨v, hv⟩ + exact ⟨v, hv.1, fun x hx => as ⟨hx.1, lt_of_le_of_lt hx.2 hv.2⟩⟩ + · rintro ⟨u, au, as⟩ + exact ⟨u, au, Subset.trans Ico_subset_Icc_self as⟩ +#align mem_nhds_within_Ici_iff_exists_Icc_subset mem_nhdsWithin_Ici_iff_exists_Icc_subset + +open List in +/-- The following statements are equivalent: + +0. `s` is a neighborhood of `b` within `(-∞, b]` +1. `s` is a neighborhood of `b` within `[a, b]` +2. `s` is a neighborhood of `b` within `(a, b]` +3. `s` includes `(l, b]` for some `l ∈ [a, b)` +4. `s` includes `(l, b]` for some `l < b` -/ +theorem TFAE_mem_nhdsWithin_Iic {a b : α} (h : a < b) (s : Set α) : + TFAE [s ∈ 𝓝[≤] b,-- 0 : `s` is a neighborhood of `b` within `(-∞, b]` + s ∈ 𝓝[Icc a b] b,-- 1 : `s` is a neighborhood of `b` within `[a, b]` + s ∈ 𝓝[Ioc a b] b,-- 2 : `s` is a neighborhood of `b` within `(a, b]` + ∃ l ∈ Ico a b, Ioc l b ⊆ s,-- 3 : `s` includes `(l, b]` for some `l ∈ [a, b)` + ∃ l ∈ Iio b, Ioc l b ⊆ s] := by-- 4 : `s` includes `(l, b]` for some `l < b` + simpa only [exists_prop, OrderDual.exists, dual_Ici, dual_Ioc, dual_Icc, dual_Ico] using + TFAE_mem_nhdsWithin_Ici h.dual (ofDual ⁻¹' s) +#align tfae_mem_nhds_within_Iic TFAE_mem_nhdsWithin_Iic + +theorem mem_nhdsWithin_Iic_iff_exists_mem_Ico_Ioc_subset {a l' : α} {s : Set α} (hl' : l' < a) : + s ∈ 𝓝[≤] a ↔ ∃ l ∈ Ico l' a, Ioc l a ⊆ s := + (TFAE_mem_nhdsWithin_Iic hl' s).out 0 3 (by norm_num) (by norm_num) +#align mem_nhds_within_Iic_iff_exists_mem_Ico_Ioc_subset mem_nhdsWithin_Iic_iff_exists_mem_Ico_Ioc_subset + +/-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `(l, a]` +with `l < a`, provided `a` is not a bottom element. -/ +theorem mem_nhdsWithin_Iic_iff_exists_Ioc_subset' {a l' : α} {s : Set α} (hl' : l' < a) : + s ∈ 𝓝[≤] a ↔ ∃ l ∈ Iio a, Ioc l a ⊆ s := + (TFAE_mem_nhdsWithin_Iic hl' s).out 0 4 (by norm_num) (by norm_num) +#align mem_nhds_within_Iic_iff_exists_Ioc_subset' mem_nhdsWithin_Iic_iff_exists_Ioc_subset' + +/-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `(l, a]` +with `l < a`. -/ +theorem mem_nhdsWithin_Iic_iff_exists_Ioc_subset [NoMinOrder α] {a : α} {s : Set α} : + s ∈ 𝓝[≤] a ↔ ∃ l ∈ Iio a, Ioc l a ⊆ s := + let ⟨_, hl'⟩ := exists_lt a + mem_nhdsWithin_Iic_iff_exists_Ioc_subset' hl' +#align mem_nhds_within_Iic_iff_exists_Ioc_subset mem_nhdsWithin_Iic_iff_exists_Ioc_subset + +/-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `[l, a]` +with `l < a`. -/ +theorem mem_nhdsWithin_Iic_iff_exists_Icc_subset [NoMinOrder α] [DenselyOrdered α] {a : α} + {s : Set α} : s ∈ 𝓝[≤] a ↔ ∃ l, l < a ∧ Icc l a ⊆ s := + calc s ∈ 𝓝[≤] a ↔ ofDual ⁻¹' s ∈ 𝓝[≥] (toDual a) := Iff.rfl + _ ↔ ∃ u : α, toDual a < toDual u ∧ Icc (toDual a) (toDual u) ⊆ ofDual ⁻¹' s := + mem_nhdsWithin_Ici_iff_exists_Icc_subset + _ ↔ ∃ l, l < a ∧ Icc l a ⊆ s := by simp only [dual_Icc]; rfl +#align mem_nhds_within_Iic_iff_exists_Icc_subset mem_nhdsWithin_Iic_iff_exists_Icc_subset + +end OrderTopology + +end LinearOrder + +section LinearOrderedAddCommGroup + +variable [TopologicalSpace α] [LinearOrderedAddCommGroup α] [OrderTopology α] + +variable {l : Filter β} {f g : β → α} + +theorem nhds_eq_infᵢ_abs_sub (a : α) : 𝓝 a = ⨅ r > 0, 𝓟 { b | |a - b| < r } := by + simp only [nhds_eq_order, abs_lt, setOf_and, ← inf_principal, infᵢ_inf_eq] + refine (congr_arg₂ _ ?_ ?_).trans inf_comm + · refine (Equiv.subLeft a).infᵢ_congr fun x => ?_; simp [Ioi] + · refine (Equiv.subRight a).infᵢ_congr fun x => ?_; simp [Iio] +#align nhds_eq_infi_abs_sub nhds_eq_infᵢ_abs_sub + +theorem orderTopology_of_nhds_abs {α : Type _} [TopologicalSpace α] [LinearOrderedAddCommGroup α] + (h_nhds : ∀ a : α, 𝓝 a = ⨅ r > 0, 𝓟 { b | |a - b| < r }) : OrderTopology α := by + refine' ⟨eq_of_nhds_eq_nhds fun a => _⟩ + rw [h_nhds] + letI := Preorder.topology α; letI : OrderTopology α := ⟨rfl⟩ + exact (nhds_eq_infᵢ_abs_sub a).symm +#align order_topology_of_nhds_abs orderTopology_of_nhds_abs + +theorem LinearOrderedAddCommGroup.tendsto_nhds {x : Filter β} {a : α} : + Tendsto f x (𝓝 a) ↔ ∀ ε > (0 : α), ∀ᶠ b in x, |f b - a| < ε := by + simp [nhds_eq_infᵢ_abs_sub, abs_sub_comm a] +#align linear_ordered_add_comm_group.tendsto_nhds LinearOrderedAddCommGroup.tendsto_nhds + +theorem eventually_abs_sub_lt (a : α) {ε : α} (hε : 0 < ε) : ∀ᶠ x in 𝓝 a, |x - a| < ε := + (nhds_eq_infᵢ_abs_sub a).symm ▸ + mem_infᵢ_of_mem ε (mem_infᵢ_of_mem hε <| by simp only [abs_sub_comm, mem_principal_self]) +#align eventually_abs_sub_lt eventually_abs_sub_lt + +/-- In a linearly ordered additive commutative group with the order topology, if `f` tends to `C` +and `g` tends to `atTop` then `f + g` tends to `atTop`. -/ +theorem Filter.Tendsto.add_atTop {C : α} (hf : Tendsto f l (𝓝 C)) (hg : Tendsto g l atTop) : + Tendsto (fun x => f x + g x) l atTop := by + nontriviality α + obtain ⟨C', hC'⟩ : ∃ C', C' < C := exists_lt C + refine' tendsto_atTop_add_left_of_le' _ C' _ hg + exact (hf.eventually (lt_mem_nhds hC')).mono fun x => le_of_lt +#align filter.tendsto.add_at_top Filter.Tendsto.add_atTop + +/-- In a linearly ordered additive commutative group with the order topology, if `f` tends to `C` +and `g` tends to `atBot` then `f + g` tends to `atBot`. -/ +theorem Filter.Tendsto.add_atBot {C : α} (hf : Tendsto f l (𝓝 C)) (hg : Tendsto g l atBot) : + Tendsto (fun x => f x + g x) l atBot := + @Filter.Tendsto.add_atTop αᵒᵈ _ _ _ _ _ _ _ _ hf hg +#align filter.tendsto.add_at_bot Filter.Tendsto.add_atBot + +/-- In a linearly ordered additive commutative group with the order topology, if `f` tends to +`atTop` and `g` tends to `C` then `f + g` tends to `atTop`. -/ +theorem Filter.Tendsto.atTop_add {C : α} (hf : Tendsto f l atTop) (hg : Tendsto g l (𝓝 C)) : + Tendsto (fun x => f x + g x) l atTop := by + conv in _ + _ => rw [add_comm] + exact hg.add_atTop hf +#align filter.tendsto.at_top_add Filter.Tendsto.atTop_add + +/-- In a linearly ordered additive commutative group with the order topology, if `f` tends to +`atBot` and `g` tends to `C` then `f + g` tends to `atBot`. -/ +theorem Filter.Tendsto.atBot_add {C : α} (hf : Tendsto f l atBot) (hg : Tendsto g l (𝓝 C)) : + Tendsto (fun x => f x + g x) l atBot := by + conv in _ + _ => rw [add_comm] + exact hg.add_atBot hf +#align filter.tendsto.at_bot_add Filter.Tendsto.atBot_add + +theorem nhds_basis_abs_sub_lt [NoMaxOrder α] (a : α) : + (𝓝 a).HasBasis (fun ε : α => (0 : α) < ε) fun ε => { b | |b - a| < ε } := by + simp only [nhds_eq_infᵢ_abs_sub, abs_sub_comm (a := a)] + refine hasBasis_binfᵢ_principal' (fun x hx y hy => ?_) (exists_gt _) + exact ⟨min x y, lt_min hx hy, fun _ hz => hz.trans_le (min_le_left _ _), + fun _ hz => hz.trans_le (min_le_right _ _)⟩ +#align nhds_basis_abs_sub_lt nhds_basis_abs_sub_lt + +theorem nhds_basis_Ioo_pos [NoMaxOrder α] (a : α) : + (𝓝 a).HasBasis (fun ε : α => (0 : α) < ε) fun ε => Ioo (a - ε) (a + ε) := by + convert nhds_basis_abs_sub_lt a + simp only [Ioo, abs_lt, ← sub_lt_iff_lt_add, neg_lt_sub_iff_lt_add, sub_lt_comm] +#align nhds_basis_Ioo_pos nhds_basis_Ioo_pos + +variable (α) + +theorem nhds_basis_zero_abs_sub_lt [NoMaxOrder α] : + (𝓝 (0 : α)).HasBasis (fun ε : α => (0 : α) < ε) fun ε => { b | |b| < ε } := by + simpa using nhds_basis_abs_sub_lt (0 : α) +#align nhds_basis_zero_abs_sub_lt nhds_basis_zero_abs_sub_lt + +variable {α} + +/-- If `a` is positive we can form a basis from only nonnegative `Set.Ioo` intervals -/ +theorem nhds_basis_Ioo_pos_of_pos [NoMaxOrder α] {a : α} (ha : 0 < a) : + (𝓝 a).HasBasis (fun ε : α => (0 : α) < ε ∧ ε ≤ a) fun ε => Ioo (a - ε) (a + ε) := + (nhds_basis_Ioo_pos a).restrict fun ε hε => ⟨min a ε, lt_min ha hε, min_le_left _ _, + Ioo_subset_Ioo (sub_le_sub_left (min_le_right _ _) _) (add_le_add_left (min_le_right _ _) _)⟩ +#align nhds_basis_Ioo_pos_of_pos nhds_basis_Ioo_pos_of_pos + +end LinearOrderedAddCommGroup + +@[deprecated image_neg] +theorem preimage_neg [AddGroup α] : preimage (Neg.neg : α → α) = image (Neg.neg : α → α) := + funext fun _ => image_neg.symm +#align preimage_neg preimage_neg + +@[deprecated] -- use `Filter.map_neg` from `Mathlib.Order.Filter.Pointwise` +theorem Filter.map_neg_eq_comap_neg [AddGroup α] : + map (Neg.neg : α → α) = comap (Neg.neg : α → α) := + funext fun _ => map_eq_comap_of_inverse (funext neg_neg) (funext neg_neg) +#align filter.map_neg_eq_comap_neg Filter.map_neg_eq_comap_neg + +section OrderTopology + +variable [TopologicalSpace α] [TopologicalSpace β] [LinearOrder α] [LinearOrder β] [OrderTopology α] + [OrderTopology β] + +theorem IsLUB.frequently_mem {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) : + ∃ᶠ x in 𝓝[≤] a, x ∈ s := by + rcases hs with ⟨a', ha'⟩ + intro h + rcases(ha.1 ha').eq_or_lt with (rfl | ha'a) + · exact h.self_of_nhdsWithin le_rfl ha' + · rcases (mem_nhdsWithin_Iic_iff_exists_Ioc_subset' ha'a).1 h with ⟨b, hba, hb⟩ + rcases ha.exists_between hba with ⟨b', hb's, hb'⟩ + exact hb hb' hb's +#align is_lub.frequently_mem IsLUB.frequently_mem + +theorem IsLUB.frequently_nhds_mem {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) : + ∃ᶠ x in 𝓝 a, x ∈ s := + (ha.frequently_mem hs).filter_mono inf_le_left +#align is_lub.frequently_nhds_mem IsLUB.frequently_nhds_mem + +theorem IsGLB.frequently_mem {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) : + ∃ᶠ x in 𝓝[≥] a, x ∈ s := + @IsLUB.frequently_mem αᵒᵈ _ _ _ _ _ ha hs +#align is_glb.frequently_mem IsGLB.frequently_mem + +theorem IsGLB.frequently_nhds_mem {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) : + ∃ᶠ x in 𝓝 a, x ∈ s := + (ha.frequently_mem hs).filter_mono inf_le_left +#align is_glb.frequently_nhds_mem IsGLB.frequently_nhds_mem + +theorem IsLUB.mem_closure {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) : a ∈ closure s := + (ha.frequently_nhds_mem hs).mem_closure +#align is_lub.mem_closure IsLUB.mem_closure + +theorem IsGLB.mem_closure {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) : a ∈ closure s := + (ha.frequently_nhds_mem hs).mem_closure +#align is_glb.mem_closure IsGLB.mem_closure + +theorem IsLUB.nhdsWithin_neBot {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) : + NeBot (𝓝[s] a) := + mem_closure_iff_nhdsWithin_neBot.1 (ha.mem_closure hs) +#align is_lub.nhds_within_ne_bot IsLUB.nhdsWithin_neBot + +theorem IsGLB.nhdsWithin_neBot : ∀ {a : α} {s : Set α}, IsGLB s a → s.Nonempty → NeBot (𝓝[s] a) := + @IsLUB.nhdsWithin_neBot αᵒᵈ _ _ _ +#align is_glb.nhds_within_ne_bot IsGLB.nhdsWithin_neBot + +theorem isLUB_of_mem_nhds {s : Set α} {a : α} {f : Filter α} (hsa : a ∈ upperBounds s) (hsf : s ∈ f) + [NeBot (f ⊓ 𝓝 a)] : IsLUB s a := + ⟨hsa, fun b hb => + not_lt.1 fun hba => + have : s ∩ { a | b < a } ∈ f ⊓ 𝓝 a := inter_mem_inf hsf (IsOpen.mem_nhds (isOpen_lt' _) hba) + let ⟨_x, ⟨hxs, hxb⟩⟩ := Filter.nonempty_of_mem this + have : b < b := lt_of_lt_of_le hxb <| hb hxs + lt_irrefl b this⟩ +#align is_lub_of_mem_nhds isLUB_of_mem_nhds + +theorem isLUB_of_mem_closure {s : Set α} {a : α} (hsa : a ∈ upperBounds s) (hsf : a ∈ closure s) : + IsLUB s a := by + rw [mem_closure_iff_clusterPt, ClusterPt, inf_comm] at hsf + exact isLUB_of_mem_nhds hsa (mem_principal_self s) +#align is_lub_of_mem_closure isLUB_of_mem_closure + +theorem isGLB_of_mem_nhds : + ∀ {s : Set α} {a : α} {f : Filter α}, a ∈ lowerBounds s → s ∈ f → NeBot (f ⊓ 𝓝 a) → IsGLB s a := + @isLUB_of_mem_nhds αᵒᵈ _ _ _ +#align is_glb_of_mem_nhds isGLB_of_mem_nhds + +theorem isGLB_of_mem_closure {s : Set α} {a : α} (hsa : a ∈ lowerBounds s) (hsf : a ∈ closure s) : + IsGLB s a := + @isLUB_of_mem_closure αᵒᵈ _ _ _ s a hsa hsf +#align is_glb_of_mem_closure isGLB_of_mem_closure + +theorem IsLUB.mem_upperBounds_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] + {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsLUB s a) + (hb : Tendsto f (𝓝[s] a) (𝓝 b)) : b ∈ upperBounds (f '' s) := by + rintro _ ⟨x, hx, rfl⟩ + replace ha := ha.inter_Ici_of_mem hx + haveI := ha.nhdsWithin_neBot ⟨x, hx, le_rfl⟩ + refine' ge_of_tendsto (hb.mono_left (nhdsWithin_mono _ (inter_subset_left s (Ici x)))) _ + exact mem_of_superset self_mem_nhdsWithin fun y hy => hf hx hy.1 hy.2 +#align is_lub.mem_upper_bounds_of_tendsto IsLUB.mem_upperBounds_of_tendsto + +-- For a version of this theorem in which the convergence considered on the domain `α` is as `x : α` +-- tends to infinity, rather than tending to a point `x` in `α`, see `isLUB_of_tendsto_atTop` +theorem IsLUB.isLUB_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} + {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsLUB s a) (hs : s.Nonempty) + (hb : Tendsto f (𝓝[s] a) (𝓝 b)) : IsLUB (f '' s) b := + haveI := ha.nhdsWithin_neBot hs + ⟨ha.mem_upperBounds_of_tendsto hf hb, fun _b' hb' => + le_of_tendsto hb (mem_of_superset self_mem_nhdsWithin fun _ hx => hb' <| mem_image_of_mem _ hx)⟩ +#align is_lub.is_lub_of_tendsto IsLUB.isLUB_of_tendsto + +theorem IsGLB.mem_lowerBounds_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] + {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsGLB s a) + (hb : Tendsto f (𝓝[s] a) (𝓝 b)) : b ∈ lowerBounds (f '' s) := + @IsLUB.mem_upperBounds_of_tendsto αᵒᵈ γᵒᵈ _ _ _ _ _ _ _ _ _ _ hf.dual ha hb +#align is_glb.mem_lower_bounds_of_tendsto IsGLB.mem_lowerBounds_of_tendsto + +-- For a version of this theorem in which the convergence considered on the domain `α` is as +-- `x : α` tends to negative infinity, rather than tending to a point `x` in `α`, see +-- `isGLB_of_tendsto_atBot` +theorem IsGLB.isGLB_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} + {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) : + IsGLB s a → s.Nonempty → Tendsto f (𝓝[s] a) (𝓝 b) → IsGLB (f '' s) b := + @IsLUB.isLUB_of_tendsto αᵒᵈ γᵒᵈ _ _ _ _ _ _ f s a b hf.dual +#align is_glb.is_glb_of_tendsto IsGLB.isGLB_of_tendsto + +theorem IsLUB.mem_lowerBounds_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] + {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : AntitoneOn f s) (ha : IsLUB s a) + (hb : Tendsto f (𝓝[s] a) (𝓝 b)) : b ∈ lowerBounds (f '' s) := + @IsLUB.mem_upperBounds_of_tendsto α γᵒᵈ _ _ _ _ _ _ _ _ _ _ hf ha hb +#align is_lub.mem_lower_bounds_of_tendsto IsLUB.mem_lowerBounds_of_tendsto + +theorem IsLUB.isGLB_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] : + ∀ {f : α → γ} {s : Set α} {a : α} {b : γ}, + AntitoneOn f s → IsLUB s a → s.Nonempty → Tendsto f (𝓝[s] a) (𝓝 b) → IsGLB (f '' s) b := + @IsLUB.isLUB_of_tendsto α γᵒᵈ _ _ _ _ _ _ +#align is_lub.is_glb_of_tendsto IsLUB.isGLB_of_tendsto + +theorem IsGLB.mem_upperBounds_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] + {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : AntitoneOn f s) (ha : IsGLB s a) + (hb : Tendsto f (𝓝[s] a) (𝓝 b)) : b ∈ upperBounds (f '' s) := + @IsGLB.mem_lowerBounds_of_tendsto α γᵒᵈ _ _ _ _ _ _ _ _ _ _ hf ha hb +#align is_glb.mem_upper_bounds_of_tendsto IsGLB.mem_upperBounds_of_tendsto + +theorem IsGLB.isLUB_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] : + ∀ {f : α → γ} {s : Set α} {a : α} {b : γ}, + AntitoneOn f s → IsGLB s a → s.Nonempty → Tendsto f (𝓝[s] a) (𝓝 b) → IsLUB (f '' s) b := + @IsGLB.isGLB_of_tendsto α γᵒᵈ _ _ _ _ _ _ +#align is_glb.is_lub_of_tendsto IsGLB.isLUB_of_tendsto + +theorem IsLUB.mem_of_isClosed {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) + (sc : IsClosed s) : a ∈ s := + sc.closure_subset <| ha.mem_closure hs +#align is_lub.mem_of_is_closed IsLUB.mem_of_isClosed + +alias IsLUB.mem_of_isClosed ← IsClosed.isLUB_mem +#align is_closed.is_lub_mem IsClosed.isLUB_mem + +theorem IsGLB.mem_of_isClosed {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) + (sc : IsClosed s) : a ∈ s := + sc.closure_subset <| ha.mem_closure hs +#align is_glb.mem_of_is_closed IsGLB.mem_of_isClosed + +alias IsGLB.mem_of_isClosed ← IsClosed.isGLB_mem +#align is_closed.is_glb_mem IsClosed.isGLB_mem + +/-! +### Existence of sequences tending to Inf or Sup of a given set +-/ + +theorem IsLUB.exists_seq_strictMono_tendsto_of_not_mem {t : Set α} {x : α} + [IsCountablyGenerated (𝓝 x)] (htx : IsLUB t x) (not_mem : x ∉ t) (ht : t.Nonempty) : + ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ n, u n ∈ t := by + obtain ⟨v, hvx, hvt⟩ := exists_seq_forall_of_frequently (htx.frequently_mem ht) + replace hvx := hvx.mono_right nhdsWithin_le_nhds + have hvx' : ∀ {n}, v n < x := (htx.1 (hvt _)).lt_of_ne (ne_of_mem_of_not_mem (hvt _) not_mem) + have : ∀ k, ∀ᶠ l in atTop, v k < v l := fun k => hvx.eventually (lt_mem_nhds hvx') + choose N hN hvN using fun k => ((eventually_gt_atTop k).and (this k)).exists + refine ⟨fun k => v ((N^[k]) 0), strictMono_nat_of_lt_succ fun _ => ?_, fun _ => hvx', + hvx.comp (strictMono_nat_of_lt_succ fun _ => ?_).tendsto_atTop, fun _ => hvt _⟩ + · rw [iterate_succ_apply']; exact hvN _ + · rw [iterate_succ_apply']; exact hN _ +#align is_lub.exists_seq_strict_mono_tendsto_of_not_mem IsLUB.exists_seq_strictMono_tendsto_of_not_mem + +theorem IsLUB.exists_seq_monotone_tendsto {t : Set α} {x : α} [IsCountablyGenerated (𝓝 x)] + (htx : IsLUB t x) (ht : t.Nonempty) : + ∃ u : ℕ → α, Monotone u ∧ (∀ n, u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ n, u n ∈ t := by + by_cases h : x ∈ t + · exact ⟨fun _ => x, monotone_const, fun n => le_rfl, tendsto_const_nhds, fun _ => h⟩ + · rcases htx.exists_seq_strictMono_tendsto_of_not_mem h ht with ⟨u, hu⟩ + exact ⟨u, hu.1.monotone, fun n => (hu.2.1 n).le, hu.2.2⟩ +#align is_lub.exists_seq_monotone_tendsto IsLUB.exists_seq_monotone_tendsto + +theorem exists_seq_strictMono_tendsto' {α : Type _} [LinearOrder α] [TopologicalSpace α] + [DenselyOrdered α] [OrderTopology α] [FirstCountableTopology α] {x y : α} (hy : y < x) : + ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x) := by + have hx : x ∉ Ioo y x := fun h => (lt_irrefl x h.2).elim + have ht : Set.Nonempty (Ioo y x) := nonempty_Ioo.2 hy + rcases(isLUB_Ioo hy).exists_seq_strictMono_tendsto_of_not_mem hx ht with ⟨u, hu⟩ + exact ⟨u, hu.1, hu.2.2.symm⟩ +#align exists_seq_strict_mono_tendsto' exists_seq_strictMono_tendsto' + +theorem exists_seq_strictMono_tendsto [DenselyOrdered α] [NoMinOrder α] [FirstCountableTopology α] + (x : α) : ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n < x) ∧ Tendsto u atTop (𝓝 x) := by + obtain ⟨y, hy⟩ : ∃ y, y < x := exists_lt x + rcases exists_seq_strictMono_tendsto' hy with ⟨u, hu_mono, hu_mem, hux⟩ + exact ⟨u, hu_mono, fun n => (hu_mem n).2, hux⟩ +#align exists_seq_strict_mono_tendsto exists_seq_strictMono_tendsto + +theorem exists_seq_strictMono_tendsto_nhdsWithin [DenselyOrdered α] [NoMinOrder α] + [FirstCountableTopology α] (x : α) : + ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n < x) ∧ Tendsto u atTop (𝓝[<] x) := + let ⟨u, hu, hx, h⟩ := exists_seq_strictMono_tendsto x + ⟨u, hu, hx, tendsto_nhdsWithin_mono_right (range_subset_iff.2 hx) <| tendsto_nhdsWithin_range.2 h⟩ +#align exists_seq_strict_mono_tendsto_nhds_within exists_seq_strictMono_tendsto_nhdsWithin + +theorem exists_seq_tendsto_supₛ {α : Type _} [ConditionallyCompleteLinearOrder α] + [TopologicalSpace α] [OrderTopology α] [FirstCountableTopology α] {S : Set α} (hS : S.Nonempty) + (hS' : BddAbove S) : ∃ u : ℕ → α, Monotone u ∧ Tendsto u atTop (𝓝 (supₛ S)) ∧ ∀ n, u n ∈ S := by + rcases(isLUB_csupₛ hS hS').exists_seq_monotone_tendsto hS with ⟨u, hu⟩ + exact ⟨u, hu.1, hu.2.2⟩ +#align exists_seq_tendsto_Sup exists_seq_tendsto_supₛ + +theorem IsGLB.exists_seq_strictAnti_tendsto_of_not_mem {t : Set α} {x : α} + [IsCountablyGenerated (𝓝 x)] (htx : IsGLB t x) (not_mem : x ∉ t) (ht : t.Nonempty) : + ∃ u : ℕ → α, StrictAnti u ∧ (∀ n, x < u n) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ n, u n ∈ t := + @IsLUB.exists_seq_strictMono_tendsto_of_not_mem αᵒᵈ _ _ _ t x _ htx not_mem ht +#align is_glb.exists_seq_strict_anti_tendsto_of_not_mem IsGLB.exists_seq_strictAnti_tendsto_of_not_mem + +theorem IsGLB.exists_seq_antitone_tendsto {t : Set α} {x : α} [IsCountablyGenerated (𝓝 x)] + (htx : IsGLB t x) (ht : t.Nonempty) : + ∃ u : ℕ → α, Antitone u ∧ (∀ n, x ≤ u n) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ n, u n ∈ t := + @IsLUB.exists_seq_monotone_tendsto αᵒᵈ _ _ _ t x _ htx ht +#align is_glb.exists_seq_antitone_tendsto IsGLB.exists_seq_antitone_tendsto + +theorem exists_seq_strictAnti_tendsto' [DenselyOrdered α] [FirstCountableTopology α] {x y : α} + (hy : x < y) : ∃ u : ℕ → α, StrictAnti u ∧ (∀ n, u n ∈ Ioo x y) ∧ Tendsto u atTop (𝓝 x) := by + simpa only [dual_Ioo] + using exists_seq_strictMono_tendsto' (α := αᵒᵈ) (OrderDual.toDual_lt_toDual.2 hy) +#align exists_seq_strict_anti_tendsto' exists_seq_strictAnti_tendsto' + +theorem exists_seq_strictAnti_tendsto [DenselyOrdered α] [NoMaxOrder α] [FirstCountableTopology α] + (x : α) : ∃ u : ℕ → α, StrictAnti u ∧ (∀ n, x < u n) ∧ Tendsto u atTop (𝓝 x) := + @exists_seq_strictMono_tendsto αᵒᵈ _ _ _ _ _ _ x +#align exists_seq_strict_anti_tendsto exists_seq_strictAnti_tendsto + +theorem exists_seq_strictAnti_tendsto_nhdsWithin [DenselyOrdered α] [NoMaxOrder α] + [FirstCountableTopology α] (x : α) : + ∃ u : ℕ → α, StrictAnti u ∧ (∀ n, x < u n) ∧ Tendsto u atTop (𝓝[>] x) := + @exists_seq_strictMono_tendsto_nhdsWithin αᵒᵈ _ _ _ _ _ _ _ +#align exists_seq_strict_anti_tendsto_nhds_within exists_seq_strictAnti_tendsto_nhdsWithin + +theorem exists_seq_strictAnti_strictMono_tendsto [DenselyOrdered α] [FirstCountableTopology α] + {x y : α} (h : x < y) : + ∃ u v : ℕ → α, StrictAnti u ∧ StrictMono v ∧ (∀ k, u k ∈ Ioo x y) ∧ (∀ l, v l ∈ Ioo x y) ∧ + (∀ k l, u k < v l) ∧ Tendsto u atTop (𝓝 x) ∧ Tendsto v atTop (𝓝 y) := by + rcases exists_seq_strictAnti_tendsto' h with ⟨u, hu_anti, hu_mem, hux⟩ + rcases exists_seq_strictMono_tendsto' (hu_mem 0).2 with ⟨v, hv_mono, hv_mem, hvy⟩ + exact + ⟨u, v, hu_anti, hv_mono, hu_mem, fun l => ⟨(hu_mem 0).1.trans (hv_mem l).1, (hv_mem l).2⟩, + fun k l => (hu_anti.antitone (zero_le k)).trans_lt (hv_mem l).1, hux, hvy⟩ +#align exists_seq_strict_anti_strict_mono_tendsto exists_seq_strictAnti_strictMono_tendsto + +theorem exists_seq_tendsto_infₛ {α : Type _} [ConditionallyCompleteLinearOrder α] + [TopologicalSpace α] [OrderTopology α] [FirstCountableTopology α] {S : Set α} (hS : S.Nonempty) + (hS' : BddBelow S) : ∃ u : ℕ → α, Antitone u ∧ Tendsto u atTop (𝓝 (infₛ S)) ∧ ∀ n, u n ∈ S := + @exists_seq_tendsto_supₛ αᵒᵈ _ _ _ _ S hS hS' +#align exists_seq_tendsto_Inf exists_seq_tendsto_infₛ + +end OrderTopology + +section DenselyOrdered + +variable [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α} + {s : Set α} + +/-- The closure of the interval `(a, +∞)` is the closed interval `[a, +∞)`, unless `a` is a top +element. -/ +theorem closure_Ioi' {a : α} (h : (Ioi a).Nonempty) : closure (Ioi a) = Ici a := by + apply Subset.antisymm + · exact closure_minimal Ioi_subset_Ici_self isClosed_Ici + · rw [← diff_subset_closure_iff, Ici_diff_Ioi_same, singleton_subset_iff] + exact isGLB_Ioi.mem_closure h +#align closure_Ioi' closure_Ioi' + +/-- The closure of the interval `(a, +∞)` is the closed interval `[a, +∞)`. -/ +@[simp] +theorem closure_Ioi (a : α) [NoMaxOrder α] : closure (Ioi a) = Ici a := + closure_Ioi' nonempty_Ioi +#align closure_Ioi closure_Ioi + +/-- The closure of the interval `(-∞, a)` is the closed interval `(-∞, a]`, unless `a` is a bottom +element. -/ +theorem closure_Iio' (h : (Iio a).Nonempty) : closure (Iio a) = Iic a := + @closure_Ioi' αᵒᵈ _ _ _ _ _ h +#align closure_Iio' closure_Iio' + +/-- The closure of the interval `(-∞, a)` is the interval `(-∞, a]`. -/ +@[simp] +theorem closure_Iio (a : α) [NoMinOrder α] : closure (Iio a) = Iic a := + closure_Iio' nonempty_Iio +#align closure_Iio closure_Iio + +/-- The closure of the open interval `(a, b)` is the closed interval `[a, b]`. -/ +@[simp] +theorem closure_Ioo {a b : α} (hab : a ≠ b) : closure (Ioo a b) = Icc a b := by + apply Subset.antisymm + · exact closure_minimal Ioo_subset_Icc_self isClosed_Icc + · cases' hab.lt_or_lt with hab hab + · rw [← diff_subset_closure_iff, Icc_diff_Ioo_same hab.le] + have hab' : (Ioo a b).Nonempty := nonempty_Ioo.2 hab + simp only [insert_subset, singleton_subset_iff] + exact ⟨(isGLB_Ioo hab).mem_closure hab', (isLUB_Ioo hab).mem_closure hab'⟩ + · rw [Icc_eq_empty_of_lt hab] + exact empty_subset _ +#align closure_Ioo closure_Ioo + +/-- The closure of the interval `(a, b]` is the closed interval `[a, b]`. -/ +@[simp] +theorem closure_Ioc {a b : α} (hab : a ≠ b) : closure (Ioc a b) = Icc a b := by + apply Subset.antisymm + · exact closure_minimal Ioc_subset_Icc_self isClosed_Icc + · apply Subset.trans _ (closure_mono Ioo_subset_Ioc_self) + rw [closure_Ioo hab] +#align closure_Ioc closure_Ioc + +/-- The closure of the interval `[a, b)` is the closed interval `[a, b]`. -/ +@[simp] +theorem closure_Ico {a b : α} (hab : a ≠ b) : closure (Ico a b) = Icc a b := by + apply Subset.antisymm + · exact closure_minimal Ico_subset_Icc_self isClosed_Icc + · apply Subset.trans _ (closure_mono Ioo_subset_Ico_self) + rw [closure_Ioo hab] +#align closure_Ico closure_Ico + +@[simp] +theorem interior_Ici' {a : α} (ha : (Iio a).Nonempty) : interior (Ici a) = Ioi a := by + rw [← compl_Iio, interior_compl, closure_Iio' ha, compl_Iic] +#align interior_Ici' interior_Ici' + +theorem interior_Ici [NoMinOrder α] {a : α} : interior (Ici a) = Ioi a := + interior_Ici' nonempty_Iio +#align interior_Ici interior_Ici + +@[simp] +theorem interior_Iic' {a : α} (ha : (Ioi a).Nonempty) : interior (Iic a) = Iio a := + @interior_Ici' αᵒᵈ _ _ _ _ _ ha +#align interior_Iic' interior_Iic' + +theorem interior_Iic [NoMaxOrder α] {a : α} : interior (Iic a) = Iio a := + interior_Iic' nonempty_Ioi +#align interior_Iic interior_Iic + +@[simp] +theorem interior_Icc [NoMinOrder α] [NoMaxOrder α] {a b : α} : interior (Icc a b) = Ioo a b := by + rw [← Ici_inter_Iic, interior_inter, interior_Ici, interior_Iic, Ioi_inter_Iio] +#align interior_Icc interior_Icc + +@[simp] +theorem interior_Ico [NoMinOrder α] {a b : α} : interior (Ico a b) = Ioo a b := by + rw [← Ici_inter_Iio, interior_inter, interior_Ici, interior_Iio, Ioi_inter_Iio] +#align interior_Ico interior_Ico + +@[simp] +theorem interior_Ioc [NoMaxOrder α] {a b : α} : interior (Ioc a b) = Ioo a b := by + rw [← Ioi_inter_Iic, interior_inter, interior_Ioi, interior_Iic, Ioi_inter_Iio] +#align interior_Ioc interior_Ioc + +theorem closure_interior_Icc {a b : α} (h : a ≠ b) : closure (interior (Icc a b)) = Icc a b := + (closure_minimal interior_subset isClosed_Icc).antisymm <| + calc + Icc a b = closure (Ioo a b) := (closure_Ioo h).symm + _ ⊆ closure (interior (Icc a b)) := + closure_mono (interior_maximal Ioo_subset_Icc_self isOpen_Ioo) +#align closure_interior_Icc closure_interior_Icc + +theorem Ioc_subset_closure_interior (a b : α) : Ioc a b ⊆ closure (interior (Ioc a b)) := by + rcases eq_or_ne a b with (rfl | h) + · simp + · calc + Ioc a b ⊆ Icc a b := Ioc_subset_Icc_self + _ = closure (Ioo a b) := (closure_Ioo h).symm + _ ⊆ closure (interior (Ioc a b)) := + closure_mono (interior_maximal Ioo_subset_Ioc_self isOpen_Ioo) +#align Ioc_subset_closure_interior Ioc_subset_closure_interior + +theorem Ico_subset_closure_interior (a b : α) : Ico a b ⊆ closure (interior (Ico a b)) := by + simpa only [dual_Ioc] using Ioc_subset_closure_interior (OrderDual.toDual b) (OrderDual.toDual a) +#align Ico_subset_closure_interior Ico_subset_closure_interior + +@[simp] +theorem frontier_Ici' {a : α} (ha : (Iio a).Nonempty) : frontier (Ici a) = {a} := by + simp [frontier, ha] +#align frontier_Ici' frontier_Ici' + +theorem frontier_Ici [NoMinOrder α] {a : α} : frontier (Ici a) = {a} := + frontier_Ici' nonempty_Iio +#align frontier_Ici frontier_Ici + +@[simp] +theorem frontier_Iic' {a : α} (ha : (Ioi a).Nonempty) : frontier (Iic a) = {a} := by + simp [frontier, ha] +#align frontier_Iic' frontier_Iic' + +theorem frontier_Iic [NoMaxOrder α] {a : α} : frontier (Iic a) = {a} := + frontier_Iic' nonempty_Ioi +#align frontier_Iic frontier_Iic + +@[simp] +theorem frontier_Ioi' {a : α} (ha : (Ioi a).Nonempty) : frontier (Ioi a) = {a} := by + simp [frontier, closure_Ioi' ha, Iic_diff_Iio, Icc_self] +#align frontier_Ioi' frontier_Ioi' + +theorem frontier_Ioi [NoMaxOrder α] {a : α} : frontier (Ioi a) = {a} := + frontier_Ioi' nonempty_Ioi +#align frontier_Ioi frontier_Ioi + +@[simp] +theorem frontier_Iio' {a : α} (ha : (Iio a).Nonempty) : frontier (Iio a) = {a} := by + simp [frontier, closure_Iio' ha, Iic_diff_Iio, Icc_self] +#align frontier_Iio' frontier_Iio' + +theorem frontier_Iio [NoMinOrder α] {a : α} : frontier (Iio a) = {a} := + frontier_Iio' nonempty_Iio +#align frontier_Iio frontier_Iio + +@[simp] +theorem frontier_Icc [NoMinOrder α] [NoMaxOrder α] {a b : α} (h : a < b) : + frontier (Icc a b) = {a, b} := by simp [frontier, le_of_lt h, Icc_diff_Ioo_same] +#align frontier_Icc frontier_Icc + +@[simp] +theorem frontier_Ioo {a b : α} (h : a < b) : frontier (Ioo a b) = {a, b} := by + rw [frontier, closure_Ioo h.ne, interior_Ioo, Icc_diff_Ioo_same h.le] +#align frontier_Ioo frontier_Ioo + +@[simp] +theorem frontier_Ico [NoMinOrder α] {a b : α} (h : a < b) : frontier (Ico a b) = {a, b} := by + rw [frontier, closure_Ico h.ne, interior_Ico, Icc_diff_Ioo_same h.le] +#align frontier_Ico frontier_Ico + +@[simp] +theorem frontier_Ioc [NoMaxOrder α] {a b : α} (h : a < b) : frontier (Ioc a b) = {a, b} := by + rw [frontier, closure_Ioc h.ne, interior_Ioc, Icc_diff_Ioo_same h.le] +#align frontier_Ioc frontier_Ioc + +theorem nhdsWithin_Ioi_neBot' {a b : α} (H₁ : (Ioi a).Nonempty) (H₂ : a ≤ b) : + NeBot (𝓝[Ioi a] b) := + mem_closure_iff_nhdsWithin_neBot.1 <| by rwa [closure_Ioi' H₁] +#align nhds_within_Ioi_ne_bot' nhdsWithin_Ioi_neBot' + +theorem nhdsWithin_Ioi_neBot [NoMaxOrder α] {a b : α} (H : a ≤ b) : NeBot (𝓝[Ioi a] b) := + nhdsWithin_Ioi_neBot' nonempty_Ioi H +#align nhds_within_Ioi_ne_bot nhdsWithin_Ioi_neBot + +theorem nhdsWithin_Ioi_self_ne_bot' {a : α} (H : (Ioi a).Nonempty) : NeBot (𝓝[>] a) := + nhdsWithin_Ioi_neBot' H (le_refl a) +#align nhds_within_Ioi_self_ne_bot' nhdsWithin_Ioi_self_ne_bot' + +@[instance] +theorem nhdsWithin_Ioi_self_neBot [NoMaxOrder α] (a : α) : NeBot (𝓝[>] a) := + nhdsWithin_Ioi_neBot (le_refl a) +#align nhds_within_Ioi_self_ne_bot nhdsWithin_Ioi_self_neBot + +theorem Filter.Eventually.exists_gt [NoMaxOrder α] {a : α} {p : α → Prop} (h : ∀ᶠ x in 𝓝 a, p x) : + ∃ b > a, p b := by + simpa only [exists_prop, gt_iff_lt, and_comm] using + ((h.filter_mono (@nhdsWithin_le_nhds _ _ a (Ioi a))).and self_mem_nhdsWithin).exists +#align filter.eventually.exists_gt Filter.Eventually.exists_gt + +theorem nhdsWithin_Iio_ne_bot' {b c : α} (H₁ : (Iio c).Nonempty) (H₂ : b ≤ c) : + NeBot (𝓝[Iio c] b) := + mem_closure_iff_nhdsWithin_neBot.1 <| by rwa [closure_Iio' H₁] +#align nhds_within_Iio_ne_bot' nhdsWithin_Iio_ne_bot' + +theorem nhdsWithin_Iio_neBot [NoMinOrder α] {a b : α} (H : a ≤ b) : NeBot (𝓝[Iio b] a) := + nhdsWithin_Iio_ne_bot' nonempty_Iio H +#align nhds_within_Iio_ne_bot nhdsWithin_Iio_neBot + +theorem nhdsWithin_Iio_self_ne_bot' {b : α} (H : (Iio b).Nonempty) : NeBot (𝓝[<] b) := + nhdsWithin_Iio_ne_bot' H (le_refl b) +#align nhds_within_Iio_self_ne_bot' nhdsWithin_Iio_self_ne_bot' + +@[instance] +theorem nhdsWithin_Iio_self_neBot [NoMinOrder α] (a : α) : NeBot (𝓝[<] a) := + nhdsWithin_Iio_neBot (le_refl a) +#align nhds_within_Iio_self_ne_bot nhdsWithin_Iio_self_neBot + +theorem Filter.Eventually.exists_lt [NoMinOrder α] {a : α} {p : α → Prop} (h : ∀ᶠ x in 𝓝 a, p x) : + ∃ b < a, p b := + @Filter.Eventually.exists_gt αᵒᵈ _ _ _ _ _ _ _ h +#align filter.eventually.exists_lt Filter.Eventually.exists_lt + +theorem right_nhdsWithin_Ico_neBot {a b : α} (H : a < b) : NeBot (𝓝[Ico a b] b) := + (isLUB_Ico H).nhdsWithin_neBot (nonempty_Ico.2 H) +#align right_nhds_within_Ico_ne_bot right_nhdsWithin_Ico_neBot + +theorem left_nhdsWithin_Ioc_neBot {a b : α} (H : a < b) : NeBot (𝓝[Ioc a b] a) := + (isGLB_Ioc H).nhdsWithin_neBot (nonempty_Ioc.2 H) +#align left_nhds_within_Ioc_ne_bot left_nhdsWithin_Ioc_neBot + +theorem left_nhdsWithin_Ioo_neBot {a b : α} (H : a < b) : NeBot (𝓝[Ioo a b] a) := + (isGLB_Ioo H).nhdsWithin_neBot (nonempty_Ioo.2 H) +#align left_nhds_within_Ioo_ne_bot left_nhdsWithin_Ioo_neBot + +theorem right_nhdsWithin_Ioo_neBot {a b : α} (H : a < b) : NeBot (𝓝[Ioo a b] b) := + (isLUB_Ioo H).nhdsWithin_neBot (nonempty_Ioo.2 H) +#align right_nhds_within_Ioo_ne_bot right_nhdsWithin_Ioo_neBot + +theorem comap_coe_nhdsWithin_Iio_of_Ioo_subset (hb : s ⊆ Iio b) + (hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s) : comap ((↑) : s → α) (𝓝[<] b) = atTop := by + nontriviality + haveI : Nonempty s := nontrivial_iff_nonempty.1 ‹_› + rcases hs (nonempty_subtype.1 ‹_›) with ⟨a, h, hs⟩ + ext u; constructor + · rintro ⟨t, ht, hts⟩ + obtain ⟨x, ⟨hxa : a ≤ x, hxb : x < b⟩, hxt : Ioo x b ⊆ t⟩ := + (mem_nhdsWithin_Iio_iff_exists_mem_Ico_Ioo_subset h).mp ht + obtain ⟨y, hxy, hyb⟩ := exists_between hxb + refine' mem_of_superset (mem_atTop ⟨y, hs ⟨hxa.trans_lt hxy, hyb⟩⟩) _ + rintro ⟨z, hzs⟩ (hyz : y ≤ z) + exact hts (hxt ⟨hxy.trans_le hyz, hb hzs⟩) + · intro hu + obtain ⟨x : s, hx : ∀ z, x ≤ z → z ∈ u⟩ := mem_atTop_sets.1 hu + exact ⟨Ioo x b, Ioo_mem_nhdsWithin_Iio' (hb x.2), fun z hz => hx _ hz.1.le⟩ +#align comap_coe_nhds_within_Iio_of_Ioo_subset comap_coe_nhdsWithin_Iio_of_Ioo_subset + +theorem comap_coe_nhdsWithin_Ioi_of_Ioo_subset (ha : s ⊆ Ioi a) + (hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s) : comap ((↑) : s → α) (𝓝[>] a) = atBot := + comap_coe_nhdsWithin_Iio_of_Ioo_subset (show ofDual ⁻¹' s ⊆ Iio (toDual a) from ha) fun h => by + simpa only [OrderDual.exists, dual_Ioo] using hs h +#align comap_coe_nhds_within_Ioi_of_Ioo_subset comap_coe_nhdsWithin_Ioi_of_Ioo_subset + +theorem map_coe_atTop_of_Ioo_subset (hb : s ⊆ Iio b) (hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s) : + map ((↑) : s → α) atTop = 𝓝[<] b := by + rcases eq_empty_or_nonempty (Iio b) with (hb' | ⟨a, ha⟩) + · have : IsEmpty s := ⟨fun x => hb'.subset (hb x.2)⟩ + rw [filter_eq_bot_of_isEmpty atTop, Filter.map_bot, hb', nhdsWithin_empty] + · rw [← comap_coe_nhdsWithin_Iio_of_Ioo_subset hb fun _ => hs a ha, map_comap_of_mem] + rw [Subtype.range_val] + exact (mem_nhdsWithin_Iio_iff_exists_Ioo_subset' ha).2 (hs a ha) +#align map_coe_at_top_of_Ioo_subset map_coe_atTop_of_Ioo_subset + +theorem map_coe_atBot_of_Ioo_subset (ha : s ⊆ Ioi a) (hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s) : + map ((↑) : s → α) atBot = 𝓝[>] a := by + -- the elaborator gets stuck without `(... : _)` + refine' (map_coe_atTop_of_Ioo_subset (show ofDual ⁻¹' s ⊆ Iio (toDual a) from ha) + fun b' hb' => _ : _) + simpa only [OrderDual.exists, dual_Ioo] using hs b' hb' +#align map_coe_at_bot_of_Ioo_subset map_coe_atBot_of_Ioo_subset + +/-- The `atTop` filter for an open interval `Ioo a b` comes from the left-neighbourhoods filter at +the right endpoint in the ambient order. -/ +theorem comap_coe_Ioo_nhdsWithin_Iio (a b : α) : comap ((↑) : Ioo a b → α) (𝓝[<] b) = atTop := + comap_coe_nhdsWithin_Iio_of_Ioo_subset Ioo_subset_Iio_self fun h => + ⟨a, nonempty_Ioo.1 h, Subset.refl _⟩ +#align comap_coe_Ioo_nhds_within_Iio comap_coe_Ioo_nhdsWithin_Iio + +/-- The `atBot` filter for an open interval `Ioo a b` comes from the right-neighbourhoods filter at +the left endpoint in the ambient order. -/ +theorem comap_coe_Ioo_nhdsWithin_Ioi (a b : α) : comap ((↑) : Ioo a b → α) (𝓝[>] a) = atBot := + comap_coe_nhdsWithin_Ioi_of_Ioo_subset Ioo_subset_Ioi_self fun h => + ⟨b, nonempty_Ioo.1 h, Subset.refl _⟩ +#align comap_coe_Ioo_nhds_within_Ioi comap_coe_Ioo_nhdsWithin_Ioi + +theorem comap_coe_Ioi_nhdsWithin_Ioi (a : α) : comap ((↑) : Ioi a → α) (𝓝[>] a) = atBot := + comap_coe_nhdsWithin_Ioi_of_Ioo_subset (Subset.refl _) fun ⟨x, hx⟩ => ⟨x, hx, Ioo_subset_Ioi_self⟩ +#align comap_coe_Ioi_nhds_within_Ioi comap_coe_Ioi_nhdsWithin_Ioi + +theorem comap_coe_Iio_nhdsWithin_Iio (a : α) : comap ((↑) : Iio a → α) (𝓝[<] a) = atTop := + @comap_coe_Ioi_nhdsWithin_Ioi αᵒᵈ _ _ _ _ a +#align comap_coe_Iio_nhds_within_Iio comap_coe_Iio_nhdsWithin_Iio + +@[simp] +theorem map_coe_Ioo_atTop {a b : α} (h : a < b) : map ((↑) : Ioo a b → α) atTop = 𝓝[<] b := + map_coe_atTop_of_Ioo_subset Ioo_subset_Iio_self fun _ _ => ⟨_, h, Subset.refl _⟩ +#align map_coe_Ioo_at_top map_coe_Ioo_atTop + +@[simp] +theorem map_coe_Ioo_atBot {a b : α} (h : a < b) : map ((↑) : Ioo a b → α) atBot = 𝓝[>] a := + map_coe_atBot_of_Ioo_subset Ioo_subset_Ioi_self fun _ _ => ⟨_, h, Subset.refl _⟩ +#align map_coe_Ioo_at_bot map_coe_Ioo_atBot + +@[simp] +theorem map_coe_Ioi_atBot (a : α) : map ((↑) : Ioi a → α) atBot = 𝓝[>] a := + map_coe_atBot_of_Ioo_subset (Subset.refl _) fun b hb => ⟨b, hb, Ioo_subset_Ioi_self⟩ +#align map_coe_Ioi_at_bot map_coe_Ioi_atBot + +@[simp] +theorem map_coe_Iio_atTop (a : α) : map ((↑) : Iio a → α) atTop = 𝓝[<] a := + @map_coe_Ioi_atBot αᵒᵈ _ _ _ _ _ +#align map_coe_Iio_at_top map_coe_Iio_atTop + +variable {l : Filter β} {f : α → β} + +@[simp] +theorem tendsto_comp_coe_Ioo_atTop (h : a < b) : + Tendsto (fun x : Ioo a b => f x) atTop l ↔ Tendsto f (𝓝[<] b) l := by + rw [← map_coe_Ioo_atTop h, tendsto_map'_iff]; rfl +#align tendsto_comp_coe_Ioo_at_top tendsto_comp_coe_Ioo_atTop + +@[simp] +theorem tendsto_comp_coe_Ioo_atBot (h : a < b) : + Tendsto (fun x : Ioo a b => f x) atBot l ↔ Tendsto f (𝓝[>] a) l := by + rw [← map_coe_Ioo_atBot h, tendsto_map'_iff]; rfl +#align tendsto_comp_coe_Ioo_at_bot tendsto_comp_coe_Ioo_atBot + +-- porting note: todo: `simpNF` claims that `simp` can't use this lemma to simplify LHS but it can +@[simp, nolint simpNF] +theorem tendsto_comp_coe_Ioi_atBot : + Tendsto (fun x : Ioi a => f x) atBot l ↔ Tendsto f (𝓝[>] a) l := by + rw [← map_coe_Ioi_atBot, tendsto_map'_iff]; rfl +#align tendsto_comp_coe_Ioi_at_bot tendsto_comp_coe_Ioi_atBot + +-- porting note: todo: `simpNF` claims that `simp` can't use this lemma to simplify LHS but it can +@[simp, nolint simpNF] +theorem tendsto_comp_coe_Iio_atTop : + Tendsto (fun x : Iio a => f x) atTop l ↔ Tendsto f (𝓝[<] a) l := by + rw [← map_coe_Iio_atTop, tendsto_map'_iff]; rfl +#align tendsto_comp_coe_Iio_at_top tendsto_comp_coe_Iio_atTop + +@[simp] +theorem tendsto_Ioo_atTop {f : β → Ioo a b} : + Tendsto f l atTop ↔ Tendsto (fun x => (f x : α)) l (𝓝[<] b) := by + rw [← comap_coe_Ioo_nhdsWithin_Iio, tendsto_comap_iff]; rfl +#align tendsto_Ioo_at_top tendsto_Ioo_atTop + +@[simp] +theorem tendsto_Ioo_atBot {f : β → Ioo a b} : + Tendsto f l atBot ↔ Tendsto (fun x => (f x : α)) l (𝓝[>] a) := by + rw [← comap_coe_Ioo_nhdsWithin_Ioi, tendsto_comap_iff]; rfl +#align tendsto_Ioo_at_bot tendsto_Ioo_atBot + +@[simp] +theorem tendsto_Ioi_atBot {f : β → Ioi a} : + Tendsto f l atBot ↔ Tendsto (fun x => (f x : α)) l (𝓝[>] a) := by + rw [← comap_coe_Ioi_nhdsWithin_Ioi, tendsto_comap_iff]; rfl +#align tendsto_Ioi_at_bot tendsto_Ioi_atBot + +@[simp] +theorem tendsto_Iio_atTop {f : β → Iio a} : + Tendsto f l atTop ↔ Tendsto (fun x => (f x : α)) l (𝓝[<] a) := by + rw [← comap_coe_Iio_nhdsWithin_Iio, tendsto_comap_iff]; rfl +#align tendsto_Iio_at_top tendsto_Iio_atTop + +instance (x : α) [Nontrivial α] : NeBot (𝓝[≠] x) := by + refine forall_mem_nonempty_iff_neBot.1 fun s hs => ?_ + obtain ⟨u, u_open, xu, us⟩ : ∃ u : Set α, IsOpen u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ s := mem_nhdsWithin.1 hs + obtain ⟨a, b, a_lt_b, hab⟩ : ∃ a b : α, a < b ∧ Ioo a b ⊆ u := u_open.exists_Ioo_subset ⟨x, xu⟩ + obtain ⟨y, hy⟩ : ∃ y, a < y ∧ y < b := exists_between a_lt_b + rcases ne_or_eq x y with (xy | rfl) + · exact ⟨y, us ⟨hab hy, xy.symm⟩⟩ + obtain ⟨z, hz⟩ : ∃ z, a < z ∧ z < x := exists_between hy.1 + exact ⟨z, us ⟨hab ⟨hz.1, hz.2.trans hy.2⟩, hz.2.ne⟩⟩ + +/-- Let `s` be a dense set in a nontrivial dense linear order `α`. If `s` is a +separable space (e.g., if `α` has a second countable topology), then there exists a countable +dense subset `t ⊆ s` such that `t` does not contain bottom/top elements of `α`. -/ +theorem Dense.exists_countable_dense_subset_no_bot_top [Nontrivial α] {s : Set α} [SeparableSpace s] + (hs : Dense s) : + ∃ t, t ⊆ s ∧ t.Countable ∧ Dense t ∧ (∀ x, IsBot x → x ∉ t) ∧ ∀ x, IsTop x → x ∉ t := by + rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩ + refine' ⟨t \ ({ x | IsBot x } ∪ { x | IsTop x }), _, _, _, fun x hx => _, fun x hx => _⟩ + · exact (diff_subset _ _).trans hts + · exact htc.mono (diff_subset _ _) + · exact htd.diff_finite ((subsingleton_isBot α).finite.union (subsingleton_isTop α).finite) + · simp [hx] + · simp [hx] +#align dense.exists_countable_dense_subset_no_bot_top Dense.exists_countable_dense_subset_no_bot_top + +variable (α) + +/-- If `α` is a nontrivial separable dense linear order, then there exists a +countable dense set `s : Set α` that contains neither top nor bottom elements of `α`. +For a dense set containing both bot and top elements, see +`exists_countable_dense_bot_top`. -/ +theorem exists_countable_dense_no_bot_top [SeparableSpace α] [Nontrivial α] : + ∃ s : Set α, s.Countable ∧ Dense s ∧ (∀ x, IsBot x → x ∉ s) ∧ ∀ x, IsTop x → x ∉ s := by + simpa using dense_univ.exists_countable_dense_subset_no_bot_top +#align exists_countable_dense_no_bot_top exists_countable_dense_no_bot_top + +end DenselyOrdered + +section CompleteLinearOrder + +variable [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] + [TopologicalSpace β] [OrderClosedTopology β] [Nonempty γ] + +theorem supₛ_mem_closure {α : Type u} [TopologicalSpace α] [CompleteLinearOrder α] [OrderTopology α] + {s : Set α} (hs : s.Nonempty) : supₛ s ∈ closure s := + (isLUB_supₛ s).mem_closure hs +#align Sup_mem_closure supₛ_mem_closure + +theorem infₛ_mem_closure {α : Type u} [TopologicalSpace α] [CompleteLinearOrder α] [OrderTopology α] + {s : Set α} (hs : s.Nonempty) : infₛ s ∈ closure s := + (isGLB_infₛ s).mem_closure hs +#align Inf_mem_closure infₛ_mem_closure + +theorem IsClosed.supₛ_mem {α : Type u} [TopologicalSpace α] [CompleteLinearOrder α] + [OrderTopology α] {s : Set α} (hs : s.Nonempty) (hc : IsClosed s) : supₛ s ∈ s := + (isLUB_supₛ s).mem_of_isClosed hs hc +#align is_closed.Sup_mem IsClosed.supₛ_mem + +theorem IsClosed.infₛ_mem {α : Type u} [TopologicalSpace α] [CompleteLinearOrder α] + [OrderTopology α] {s : Set α} (hs : s.Nonempty) (hc : IsClosed s) : infₛ s ∈ s := + (isGLB_infₛ s).mem_of_isClosed hs hc +#align is_closed.Inf_mem IsClosed.infₛ_mem + +/-- A monotone function continuous at the supremum of a nonempty set sends this supremum to +the supremum of the image of this set. -/ +theorem Monotone.map_supₛ_of_continuousAt' {f : α → β} {s : Set α} (Cf : ContinuousAt f (supₛ s)) + (Mf : Monotone f) (hs : s.Nonempty) : f (supₛ s) = supₛ (f '' s) := + ((--This is a particular case of the more general is_lub.is_lub_of_tendsto + isLUB_supₛ + _).isLUB_of_tendsto + (fun _ _ _ _ xy => Mf xy) hs <| + Cf.mono_left inf_le_left).supₛ_eq.symm +#align monotone.map_Sup_of_continuous_at' Monotone.map_supₛ_of_continuousAt' + +/-- A monotone function `f` sending `bot` to `bot` and continuous at the supremum of a set sends +this supremum to the supremum of the image of this set. -/ +theorem Monotone.map_supₛ_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (supₛ s)) + (Mf : Monotone f) (fbot : f ⊥ = ⊥) : f (supₛ s) = supₛ (f '' s) := by + cases' s.eq_empty_or_nonempty with h h + · simp [h, fbot] + · exact Mf.map_supₛ_of_continuousAt' Cf h +#align monotone.map_Sup_of_continuous_at Monotone.map_supₛ_of_continuousAt + +/-- A monotone function continuous at the indexed supremum over a nonempty `Sort` sends this indexed +supremum to the indexed supremum of the composition. -/ +theorem Monotone.map_supᵢ_of_continuousAt' {ι : Sort _} [Nonempty ι] {f : α → β} {g : ι → α} + (Cf : ContinuousAt f (supᵢ g)) (Mf : Monotone f) : f (⨆ i, g i) = ⨆ i, f (g i) := by + rw [supᵢ, Mf.map_supₛ_of_continuousAt' Cf (range_nonempty g), ← range_comp, supᵢ]; rfl +#align monotone.map_supr_of_continuous_at' Monotone.map_supᵢ_of_continuousAt' + +/-- If a monotone function sending `bot` to `bot` is continuous at the indexed supremum over +a `Sort`, then it sends this indexed supremum to the indexed supremum of the composition. -/ +theorem Monotone.map_supᵢ_of_continuousAt {ι : Sort _} {f : α → β} {g : ι → α} + (Cf : ContinuousAt f (supᵢ g)) (Mf : Monotone f) (fbot : f ⊥ = ⊥) : + f (⨆ i, g i) = ⨆ i, f (g i) := by + rw [supᵢ, Mf.map_supₛ_of_continuousAt Cf fbot, ← range_comp, supᵢ]; rfl +#align monotone.map_supr_of_continuous_at Monotone.map_supᵢ_of_continuousAt + +/-- A monotone function continuous at the infimum of a nonempty set sends this infimum to +the infimum of the image of this set. -/ +theorem Monotone.map_infₛ_of_continuousAt' {f : α → β} {s : Set α} (Cf : ContinuousAt f (infₛ s)) + (Mf : Monotone f) (hs : s.Nonempty) : f (infₛ s) = infₛ (f '' s) := + @Monotone.map_supₛ_of_continuousAt' αᵒᵈ βᵒᵈ _ _ _ _ _ _ f s Cf Mf.dual hs +#align monotone.map_Inf_of_continuous_at' Monotone.map_infₛ_of_continuousAt' + +/-- A monotone function `f` sending `top` to `top` and continuous at the infimum of a set sends +this infimum to the infimum of the image of this set. -/ +theorem Monotone.map_infₛ_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (infₛ s)) + (Mf : Monotone f) (ftop : f ⊤ = ⊤) : f (infₛ s) = infₛ (f '' s) := + @Monotone.map_supₛ_of_continuousAt αᵒᵈ βᵒᵈ _ _ _ _ _ _ f s Cf Mf.dual ftop +#align monotone.map_Inf_of_continuous_at Monotone.map_infₛ_of_continuousAt + +/-- A monotone function continuous at the indexed infimum over a nonempty `Sort` sends this indexed +infimum to the indexed infimum of the composition. -/ +theorem Monotone.map_infᵢ_of_continuousAt' {ι : Sort _} [Nonempty ι] {f : α → β} {g : ι → α} + (Cf : ContinuousAt f (infᵢ g)) (Mf : Monotone f) : f (⨅ i, g i) = ⨅ i, f (g i) := + @Monotone.map_supᵢ_of_continuousAt' αᵒᵈ βᵒᵈ _ _ _ _ _ _ ι _ f g Cf Mf.dual +#align monotone.map_infi_of_continuous_at' Monotone.map_infᵢ_of_continuousAt' + +/-- If a monotone function sending `top` to `top` is continuous at the indexed infimum over +a `Sort`, then it sends this indexed infimum to the indexed infimum of the composition. -/ +theorem Monotone.map_infᵢ_of_continuousAt {ι : Sort _} {f : α → β} {g : ι → α} + (Cf : ContinuousAt f (infᵢ g)) (Mf : Monotone f) (ftop : f ⊤ = ⊤) : f (infᵢ g) = infᵢ (f ∘ g) := + @Monotone.map_supᵢ_of_continuousAt αᵒᵈ βᵒᵈ _ _ _ _ _ _ ι f g Cf Mf.dual ftop +#align monotone.map_infi_of_continuous_at Monotone.map_infᵢ_of_continuousAt + +/-- An antitone function continuous at the supremum of a nonempty set sends this supremum to +the infimum of the image of this set. -/ +theorem Antitone.map_supₛ_of_continuousAt' {f : α → β} {s : Set α} (Cf : ContinuousAt f (supₛ s)) + (Af : Antitone f) (hs : s.Nonempty) : f (supₛ s) = infₛ (f '' s) := + Monotone.map_supₛ_of_continuousAt' (show ContinuousAt (OrderDual.toDual ∘ f) (supₛ s) from Cf) Af + hs +#align antitone.map_Sup_of_continuous_at' Antitone.map_supₛ_of_continuousAt' + +/-- An antitone function `f` sending `bot` to `top` and continuous at the supremum of a set sends +this supremum to the infimum of the image of this set. -/ +theorem Antitone.map_supₛ_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (supₛ s)) + (Af : Antitone f) (fbot : f ⊥ = ⊤) : f (supₛ s) = infₛ (f '' s) := + Monotone.map_supₛ_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (supₛ s) from Cf) Af + fbot +#align antitone.map_Sup_of_continuous_at Antitone.map_supₛ_of_continuousAt + +/-- An antitone function continuous at the indexed supremum over a nonempty `Sort` sends this +indexed supremum to the indexed infimum of the composition. -/ +theorem Antitone.map_supᵢ_of_continuousAt' {ι : Sort _} [Nonempty ι] {f : α → β} {g : ι → α} + (Cf : ContinuousAt f (supᵢ g)) (Af : Antitone f) : f (⨆ i, g i) = ⨅ i, f (g i) := + Monotone.map_supᵢ_of_continuousAt' (show ContinuousAt (OrderDual.toDual ∘ f) (supᵢ g) from Cf) Af +#align antitone.map_supr_of_continuous_at' Antitone.map_supᵢ_of_continuousAt' + +/-- An antitone function sending `bot` to `top` is continuous at the indexed supremum over +a `Sort`, then it sends this indexed supremum to the indexed supremum of the composition. -/ +theorem Antitone.map_supᵢ_of_continuousAt {ι : Sort _} {f : α → β} {g : ι → α} + (Cf : ContinuousAt f (supᵢ g)) (Af : Antitone f) (fbot : f ⊥ = ⊤) : + f (⨆ i, g i) = ⨅ i, f (g i) := + Monotone.map_supᵢ_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (supᵢ g) from Cf) Af + fbot +#align antitone.map_supr_of_continuous_at Antitone.map_supᵢ_of_continuousAt + +/-- An antitone function continuous at the infimum of a nonempty set sends this infimum to +the supremum of the image of this set. -/ +theorem Antitone.map_infₛ_of_continuousAt' {f : α → β} {s : Set α} (Cf : ContinuousAt f (infₛ s)) + (Af : Antitone f) (hs : s.Nonempty) : f (infₛ s) = supₛ (f '' s) := + Monotone.map_infₛ_of_continuousAt' (show ContinuousAt (OrderDual.toDual ∘ f) (infₛ s) from Cf) Af + hs +#align antitone.map_Inf_of_continuous_at' Antitone.map_infₛ_of_continuousAt' + +/-- An antitone function `f` sending `top` to `bot` and continuous at the infimum of a set sends +this infimum to the supremum of the image of this set. -/ +theorem Antitone.map_infₛ_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (infₛ s)) + (Af : Antitone f) (ftop : f ⊤ = ⊥) : f (infₛ s) = supₛ (f '' s) := + Monotone.map_infₛ_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (infₛ s) from Cf) Af + ftop +#align antitone.map_Inf_of_continuous_at Antitone.map_infₛ_of_continuousAt + +/-- An antitone function continuous at the indexed infimum over a nonempty `Sort` sends this indexed +infimum to the indexed supremum of the composition. -/ +theorem Antitone.map_infᵢ_of_continuousAt' {ι : Sort _} [Nonempty ι] {f : α → β} {g : ι → α} + (Cf : ContinuousAt f (infᵢ g)) (Af : Antitone f) : f (⨅ i, g i) = ⨆ i, f (g i) := + Monotone.map_infᵢ_of_continuousAt' (show ContinuousAt (OrderDual.toDual ∘ f) (infᵢ g) from Cf) Af +#align antitone.map_infi_of_continuous_at' Antitone.map_infᵢ_of_continuousAt' + +/-- If an antitone function sending `top` to `bot` is continuous at the indexed infimum over +a `Sort`, then it sends this indexed infimum to the indexed supremum of the composition. -/ +theorem Antitone.map_infᵢ_of_continuousAt {ι : Sort _} {f : α → β} {g : ι → α} + (Cf : ContinuousAt f (infᵢ g)) (Af : Antitone f) (ftop : f ⊤ = ⊥) : f (infᵢ g) = supᵢ (f ∘ g) := + Monotone.map_infᵢ_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (infᵢ g) from Cf) Af + ftop +#align antitone.map_infi_of_continuous_at Antitone.map_infᵢ_of_continuousAt + +end CompleteLinearOrder + +section ConditionallyCompleteLinearOrder + +variable [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] + [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] [Nonempty γ] + +theorem csupₛ_mem_closure {s : Set α} (hs : s.Nonempty) (B : BddAbove s) : supₛ s ∈ closure s := + (isLUB_csupₛ hs B).mem_closure hs +#align cSup_mem_closure csupₛ_mem_closure + +theorem cinfₛ_mem_closure {s : Set α} (hs : s.Nonempty) (B : BddBelow s) : infₛ s ∈ closure s := + (isGLB_cinfₛ hs B).mem_closure hs +#align cInf_mem_closure cinfₛ_mem_closure + +theorem IsClosed.csupₛ_mem {s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddAbove s) : + supₛ s ∈ s := + (isLUB_csupₛ hs B).mem_of_isClosed hs hc +#align is_closed.cSup_mem IsClosed.csupₛ_mem + +theorem IsClosed.cinfₛ_mem {s : Set α} (hc : IsClosed s) (hs : s.Nonempty) (B : BddBelow s) : + infₛ s ∈ s := + (isGLB_cinfₛ hs B).mem_of_isClosed hs hc +#align is_closed.cInf_mem IsClosed.cinfₛ_mem + +/-- If a monotone function is continuous at the supremum of a nonempty bounded above set `s`, +then it sends this supremum to the supremum of the image of `s`. -/ +theorem Monotone.map_csupₛ_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (supₛ s)) + (Mf : Monotone f) (ne : s.Nonempty) (H : BddAbove s) : f (supₛ s) = supₛ (f '' s) := by + refine' ((isLUB_csupₛ (ne.image f) (Mf.map_bddAbove H)).unique _).symm + refine' (isLUB_csupₛ ne H).isLUB_of_tendsto (fun x _ y _ xy => Mf xy) ne _ + exact Cf.mono_left inf_le_left +#align monotone.map_cSup_of_continuous_at Monotone.map_csupₛ_of_continuousAt + +/-- If a monotone function is continuous at the indexed supremum of a bounded function on +a nonempty `Sort`, then it sends this supremum to the supremum of the composition. -/ +theorem Monotone.map_csupr_of_continuousAt {f : α → β} {g : γ → α} (Cf : ContinuousAt f (⨆ i, g i)) + (Mf : Monotone f) (H : BddAbove (range g)) : f (⨆ i, g i) = ⨆ i, f (g i) := by + rw [supᵢ, Mf.map_csupₛ_of_continuousAt Cf (range_nonempty _) H, ← range_comp, supᵢ]; rfl +#align monotone.map_csupr_of_continuous_at Monotone.map_csupr_of_continuousAt + +/-- If a monotone function is continuous at the infimum of a nonempty bounded below set `s`, +then it sends this infimum to the infimum of the image of `s`. -/ +theorem Monotone.map_cinfₛ_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (infₛ s)) + (Mf : Monotone f) (ne : s.Nonempty) (H : BddBelow s) : f (infₛ s) = infₛ (f '' s) := + @Monotone.map_csupₛ_of_continuousAt αᵒᵈ βᵒᵈ _ _ _ _ _ _ f s Cf Mf.dual ne H +#align monotone.map_cInf_of_continuous_at Monotone.map_cinfₛ_of_continuousAt + +/-- A continuous monotone function sends indexed infimum to indexed infimum in conditionally +complete linear order, under a boundedness assumption. -/ +theorem Monotone.map_cinfᵢ_of_continuousAt {f : α → β} {g : γ → α} (Cf : ContinuousAt f (⨅ i, g i)) + (Mf : Monotone f) (H : BddBelow (range g)) : f (⨅ i, g i) = ⨅ i, f (g i) := + @Monotone.map_csupr_of_continuousAt αᵒᵈ βᵒᵈ _ _ _ _ _ _ _ _ _ _ Cf Mf.dual H +#align monotone.map_cinfi_of_continuous_at Monotone.map_cinfᵢ_of_continuousAt + +/-- If an antitone function is continuous at the supremum of a nonempty bounded above set `s`, +then it sends this supremum to the infimum of the image of `s`. -/ +theorem Antitone.map_csupₛ_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (supₛ s)) + (Af : Antitone f) (ne : s.Nonempty) (H : BddAbove s) : f (supₛ s) = infₛ (f '' s) := + Monotone.map_csupₛ_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (supₛ s) from Cf) Af + ne H +#align antitone.map_cSup_of_continuous_at Antitone.map_csupₛ_of_continuousAt + +/-- If an antitone function is continuous at the indexed supremum of a bounded function on +a nonempty `Sort`, then it sends this supremum to the infimum of the composition. -/ +theorem Antitone.map_csupr_of_continuousAt {f : α → β} {g : γ → α} (Cf : ContinuousAt f (⨆ i, g i)) + (Af : Antitone f) (H : BddAbove (range g)) : f (⨆ i, g i) = ⨅ i, f (g i) := + Monotone.map_csupr_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (⨆ i, g i) from Cf) + Af H +#align antitone.map_csupr_of_continuous_at Antitone.map_csupr_of_continuousAt + +/-- If an antitone function is continuous at the infimum of a nonempty bounded below set `s`, +then it sends this infimum to the supremum of the image of `s`. -/ +theorem Antitone.map_cinfₛ_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (infₛ s)) + (Af : Antitone f) (ne : s.Nonempty) (H : BddBelow s) : f (infₛ s) = supₛ (f '' s) := + Monotone.map_cinfₛ_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (infₛ s) from Cf) Af + ne H +#align antitone.map_cInf_of_continuous_at Antitone.map_cinfₛ_of_continuousAt + +/-- A continuous antitone function sends indexed infimum to indexed supremum in conditionally +complete linear order, under a boundedness assumption. -/ +theorem Antitone.map_cinfᵢ_of_continuousAt {f : α → β} {g : γ → α} (Cf : ContinuousAt f (⨅ i, g i)) + (Af : Antitone f) (H : BddBelow (range g)) : f (⨅ i, g i) = ⨆ i, f (g i) := + Monotone.map_cinfᵢ_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (⨅ i, g i) from Cf) + Af H +#align antitone.map_cinfi_of_continuous_at Antitone.map_cinfᵢ_of_continuousAt + +/-- A monotone map has a limit to the left of any point `x`, equal to `supₛ (f '' (Iio x))`. -/ +theorem Monotone.tendsto_nhdsWithin_Iio {α β : Type _} [LinearOrder α] [TopologicalSpace α] + [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] + {f : α → β} (Mf : Monotone f) (x : α) : Tendsto f (𝓝[<] x) (𝓝 (supₛ (f '' Iio x))) := by + rcases eq_empty_or_nonempty (Iio x) with (h | h); · simp [h] + refine' tendsto_order.2 ⟨fun l hl => _, fun m hm => _⟩ + · obtain ⟨z, zx, lz⟩ : ∃ a : α, a < x ∧ l < f a := by + simpa only [mem_image, exists_prop, exists_exists_and_eq_and] using + exists_lt_of_lt_csupₛ (nonempty_image_iff.2 h) hl + exact mem_of_superset (Ioo_mem_nhdsWithin_Iio' zx) fun y hy => lz.trans_le (Mf hy.1.le) + · refine mem_of_superset self_mem_nhdsWithin fun _ hy => lt_of_le_of_lt ?_ hm + exact le_csupₛ (Mf.map_bddAbove bddAbove_Iio) (mem_image_of_mem _ hy) +#align monotone.tendsto_nhds_within_Iio Monotone.tendsto_nhdsWithin_Iio + +/-- A monotone map has a limit to the right of any point `x`, equal to `infₛ (f '' (Ioi x))`. -/ +theorem Monotone.tendsto_nhdsWithin_Ioi {α β : Type _} [LinearOrder α] [TopologicalSpace α] + [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] + {f : α → β} (Mf : Monotone f) (x : α) : Tendsto f (𝓝[>] x) (𝓝 (infₛ (f '' Ioi x))) := + @Monotone.tendsto_nhdsWithin_Iio αᵒᵈ βᵒᵈ _ _ _ _ _ _ f Mf.dual x +#align monotone.tendsto_nhds_within_Ioi Monotone.tendsto_nhdsWithin_Ioi + +end ConditionallyCompleteLinearOrder + +section NhdsWithPos + +section LinearOrderedAddCommGroup + +variable [LinearOrder α] [Zero α] [TopologicalSpace α] [OrderTopology α] + +@[deprecated Ioo_mem_nhdsWithin_Ioi'] +theorem eventually_nhdsWithin_pos_mem_Ioo {ε : α} (h : 0 < ε) : ∀ᶠ x in 𝓝[>] 0, x ∈ Ioo 0 ε := + Ioo_mem_nhdsWithin_Ioi' h +#align eventually_nhds_within_pos_mem_Ioo eventually_nhdsWithin_pos_mem_Ioo + +@[deprecated Ioc_mem_nhdsWithin_Ioi'] +theorem eventually_nhdsWithin_pos_mem_Ioc {ε : α} (h : 0 < ε) : ∀ᶠ x in 𝓝[>] 0, x ∈ Ioc 0 ε := + Ioc_mem_nhdsWithin_Ioi' h +#align eventually_nhds_within_pos_mem_Ioc eventually_nhdsWithin_pos_mem_Ioc + +end LinearOrderedAddCommGroup + +end NhdsWithPos + +end OrderTopology