Mathlib.Topology.Order.IsLUB

IsLUB.frequently_mem theorem

{a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) : ∃ᶠ x in 𝓝[≤] a, x ∈ s

Full source

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_nhdsLE_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

Existence of a sequence converging to the supremum from below in an order topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $s$ be a nonempty subset of $\alpha$ with least upper bound $a$. Then there exists a sequence of points in $s$ that converges to $a$ from the left, i.e., within the neighborhood $\mathcal{N}_{\leq a}$.

IsLUB.frequently_nhds_mem theorem

{a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) : ∃ᶠ x in 𝓝 a, x ∈ s

Full source

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

Existence of a sequence converging to the supremum in an order topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $s$ be a nonempty subset of $\alpha$ with least upper bound $a$. Then there exists a sequence of points in $s$ that converges to $a$ in the neighborhood $\mathcal{N}_a$.

IsGLB.frequently_mem theorem

{a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) : ∃ᶠ x in 𝓝[≥] a, x ∈ s

Full source

theorem IsGLB.frequently_mem {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) :
    ∃ᶠ x in 𝓝[≥] a, x ∈ s :=
  IsLUB.frequently_mem (α := αᵒᵈ) ha hs

Existence of a sequence converging to the infimum from above in an order topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $s$ be a nonempty subset of $\alpha$ with greatest lower bound $a$. Then there exists a sequence of points in $s$ that converges to $a$ from the right, i.e., within the neighborhood $\mathcal{N}_{\geq a}$.

IsGLB.frequently_nhds_mem theorem

{a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) : ∃ᶠ x in 𝓝 a, x ∈ s

Full source

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

Existence of a sequence converging to the infimum in an order topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $s$ be a nonempty subset of $\alpha$ with greatest lower bound $a$. Then there exists a sequence of points in $s$ that converges to $a$ in the neighborhood $\mathcal{N}_a$.

IsLUB.mem_closure theorem

{a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) : a ∈ closure s

Full source

theorem IsLUB.mem_closure {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) : a ∈ closure s :=
  (ha.frequently_nhds_mem hs).mem_closure

Supremum is in the closure of a nonempty set in an order topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $s$ be a nonempty subset of $\alpha$ with least upper bound $a$. Then $a$ belongs to the closure of $s$.

IsGLB.mem_closure theorem

{a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) : a ∈ closure s

Full source

theorem IsGLB.mem_closure {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) : a ∈ closure s :=
  (ha.frequently_nhds_mem hs).mem_closure

Infimum is in the closure of a nonempty set in an order topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $s$ be a nonempty subset of $\alpha$ with greatest lower bound $a$. Then $a$ belongs to the closure of $s$.

IsLUB.nhdsWithin_neBot theorem

{a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) : NeBot (𝓝[s] a)

Full source

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)

Non-triviality of Neighborhood Filter at Supremum in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $s$ be a nonempty subset of $\alpha$ with least upper bound $a$. Then the neighborhood filter of $a$ within $s$ is non-trivial (i.e., contains more than just the empty set).

IsGLB.nhdsWithin_neBot theorem

{a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) : NeBot (𝓝[s] a)

Full source

theorem IsGLB.nhdsWithin_neBot {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) :
    NeBot (𝓝[s] a) :=
  IsLUB.nhdsWithin_neBot (α := αᵒᵈ) ha hs

Non-triviality of Neighborhood Filter at Infimum in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $s$ be a nonempty subset of $\alpha$ with greatest lower bound $a$. Then the neighborhood filter of $a$ within $s$ is non-trivial (i.e., contains more than just the empty set).

isLUB_of_mem_nhds theorem

{s : Set α} {a : α} {f : Filter α} (hsa : a ∈ upperBounds s) (hsf : s ∈ f) [NeBot (f ⊓ 𝓝 a)] : IsLUB s a

Full source

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⟩

Characterization of Least Upper Bound via Filter Convergence

Informal description

Let $s$ be a subset of a topological space $\alpha$ and $a \in \alpha$ be an upper bound of $s$. If $s$ belongs to a filter $f$ and the infimum of $f$ with the neighborhood filter of $a$ is non-trivial, then $a$ is the least upper bound of $s$.

isLUB_of_mem_closure theorem

{s : Set α} {a : α} (hsa : a ∈ upperBounds s) (hsf : a ∈ closure s) : IsLUB s a

Full source

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)

Least Upper Bound via Closure Condition

Informal description

Let $s$ be a subset of a topological space $\alpha$ and $a \in \alpha$ be an upper bound of $s$. If $a$ belongs to the closure of $s$, then $a$ is the least upper bound of $s$.

isGLB_of_mem_nhds theorem

{s : Set α} {a : α} {f : Filter α} (hsa : a ∈ lowerBounds s) (hsf : s ∈ f) [NeBot (f ⊓ 𝓝 a)] : IsGLB s a

Full source

theorem isGLB_of_mem_nhds {s : Set α} {a : α} {f : Filter α} (hsa : a ∈ lowerBounds s) (hsf : s ∈ f)
    [NeBot (f ⊓ 𝓝 a)] :
    IsGLB s a :=
  isLUB_of_mem_nhds (α := αᵒᵈ) hsa hsf

Characterization of Greatest Lower Bound via Filter Convergence

Informal description

Let $s$ be a subset of a topological space $\alpha$ and $a \in \alpha$ be a lower bound of $s$. If $s$ belongs to a filter $f$ and the infimum of $f$ with the neighborhood filter of $a$ is non-trivial, then $a$ is the greatest lower bound of $s$.

isGLB_of_mem_closure theorem

{s : Set α} {a : α} (hsa : a ∈ lowerBounds s) (hsf : a ∈ closure s) : IsGLB s a

Full source

theorem isGLB_of_mem_closure {s : Set α} {a : α} (hsa : a ∈ lowerBounds s) (hsf : a ∈ closure s) :
    IsGLB s a :=
  isLUB_of_mem_closure (α := αᵒᵈ) hsa hsf

Greatest Lower Bound via Closure Condition

Informal description

Let $s$ be a subset of a topological space $\alpha$ and $a \in \alpha$ be a lower bound of $s$. If $a$ belongs to the closure of $s$, then $a$ is the greatest lower bound of $s$.

IsLUB.mem_upperBounds_of_tendsto theorem

 [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)

Full source

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 a (inter_subset_left (t := Ici x)))) ?_
  exact mem_of_superset self_mem_nhdsWithin fun y hy => hf hx hy.1 hy.2

Convergence Preserves Upper Bounds at Supremum in Order-Closed Topology

Informal description

Let $\gamma$ be a topological space with a preorder and an order-closed topology, and let $f : \alpha \to \gamma$ be a function. Suppose $s \subseteq \alpha$ is a subset with least upper bound $a \in \alpha$, and $f$ is monotone on $s$. If $f$ converges to $b \in \gamma$ along the neighborhood filter of $a$ within $s$, then $b$ is an upper bound for the image $f(s)$.

IsLUB.isLUB_of_tendsto theorem

 [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

Full source

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)⟩

Monotone Convergence Preserves Supremum in Order-Closed Topology

Informal description

Let $\gamma$ be a topological space with a preorder and an order-closed topology, and let $f : \alpha \to \gamma$ be a function. Suppose $s \subseteq \alpha$ is a nonempty subset with least upper bound $a \in \alpha$, and $f$ is monotone on $s$. If $f$ converges to $b \in \gamma$ along the neighborhood filter of $a$ within $s$, then $b$ is the least upper bound of the image $f(s)$.

IsGLB.mem_lowerBounds_of_tendsto theorem

 [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)

Full source

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

Convergence Preserves Lower Bounds at Infimum in Order-Closed Topology

Informal description

Let $\gamma$ be a topological space with a preorder and an order-closed topology, and let $f : \alpha \to \gamma$ be a function. Suppose $s \subseteq \alpha$ is a subset with greatest lower bound $a \in \alpha$, and $f$ is monotone on $s$. If $f$ converges to $b \in \gamma$ along the neighborhood filter of $a$ within $s$, then $b$ is a lower bound for the image $f(s)$.

IsGLB.isGLB_of_tendsto theorem

 [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

Full source

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 (α := αᵒᵈ) (γ := γᵒᵈ) hf.dual

Monotone Convergence Preserves Infimum in Order-Closed Topology

Informal description

Let $\gamma$ be a topological space with a preorder and an order-closed topology, and let $f : \alpha \to \gamma$ be a function. Suppose $s \subseteq \alpha$ is a nonempty subset with greatest lower bound $a \in \alpha$, and $f$ is monotone on $s$. If $f$ converges to $b \in \gamma$ along the neighborhood filter of $a$ within $s$, then $b$ is the greatest lower bound of the image $f(s)$.

IsLUB.mem_lowerBounds_of_tendsto theorem

 [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)

Full source

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

Convergence Preserves Lower Bounds at Supremum for Antitone Functions in Order-Closed Topology

Informal description

Let $\gamma$ be a topological space with a preorder and an order-closed topology, and let $f : \alpha \to \gamma$ be a function. Suppose $s \subseteq \alpha$ is a subset with least upper bound $a \in \alpha$, and $f$ is antitone on $s$. If $f$ converges to $b \in \gamma$ along the neighborhood filter of $a$ within $s$, then $b$ is a lower bound for the image $f(s)$.

IsLUB.isGLB_of_tendsto theorem

 [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : AntitoneOn f s)
  (ha : IsLUB s a) (hs : s.Nonempty) (hb : Tendsto f (𝓝[s] a) (𝓝 b)) : IsGLB (f '' s) b

Full source

theorem IsLUB.isGLB_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ}
    {s : Set α} {a : α} {b : γ} (hf : AntitoneOn f s) (ha : IsLUB s a) (hs : s.Nonempty)
    (hb : Tendsto f (𝓝[s] a) (𝓝 b)) : IsGLB (f '' s) b :=
  IsLUB.isLUB_of_tendsto (γ := γᵒᵈ) hf ha hs hb

Antitone Convergence at Supremum Yields Infimum of Image

Informal description

Let $\gamma$ be a topological space with a preorder and an order-closed topology, and let $f : \alpha \to \gamma$ be a function. Suppose $s \subseteq \alpha$ is a nonempty subset with least upper bound $a \in \alpha$, and $f$ is antitone on $s$. If $f$ converges to $b \in \gamma$ along the neighborhood filter of $a$ within $s$, then $b$ is the greatest lower bound of the image $f(s)$.

IsGLB.mem_upperBounds_of_tendsto theorem

 [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)

Full source

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

Convergence Preserves Upper Bounds at Infimum for Antitone Functions in Order-Closed Topology

Informal description

Let $\gamma$ be a topological space with a preorder and an order-closed topology, and let $f : \alpha \to \gamma$ be a function. Suppose $s \subseteq \alpha$ is a subset with greatest lower bound $a \in \alpha$, and $f$ is antitone on $s$. If $f$ converges to $b \in \gamma$ along the neighborhood filter of $a$ within $s$, then $b$ is an upper bound for the image $f(s)$.

IsGLB.isLUB_of_tendsto theorem

 [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : AntitoneOn f s)
  (ha : IsGLB s a) (hs : s.Nonempty) (hb : Tendsto f (𝓝[s] a) (𝓝 b)) : IsLUB (f '' s) b

Full source

theorem IsGLB.isLUB_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ}
    {s : Set α} {a : α} {b : γ} (hf : AntitoneOn f s) (ha : IsGLB s a) (hs : s.Nonempty)
    (hb : Tendsto f (𝓝[s] a) (𝓝 b)) : IsLUB (f '' s) b :=
  IsGLB.isGLB_of_tendsto (γ := γᵒᵈ) hf ha hs hb

Antitone Convergence at Infimum Yields Supremum of Image

Informal description

Let $\gamma$ be a topological space with a preorder and an order-closed topology, and let $f : \alpha \to \gamma$ be a function. Suppose $s \subseteq \alpha$ is a nonempty subset with greatest lower bound $a \in \alpha$, and $f$ is antitone on $s$. If $f$ converges to $b \in \gamma$ along the neighborhood filter of $a$ within $s$, then $b$ is the least upper bound of the image $f(s)$.

IsLUB.mem_of_isClosed theorem

{a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) (sc : IsClosed s) : a ∈ s

Full source

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

Supremum of a Nonempty Closed Set Belongs to the Set

Informal description

Let $\alpha$ be a topological space with an order topology, and let $s$ be a nonempty closed subset of $\alpha$ with least upper bound $a$. Then $a$ belongs to $s$.

IsGLB.mem_of_isClosed theorem

{a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) (sc : IsClosed s) : a ∈ s

Full source

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

Infimum of a Nonempty Closed Set Belongs to the Set

Informal description

Let $\alpha$ be a topological space with an order topology, and let $s$ be a nonempty closed subset of $\alpha$ with greatest lower bound $a$. Then $a$ belongs to $s$.

isLUB_iff_of_subset_of_subset_closure theorem

 {α : Type*} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {s t : Set α} (hst : s ⊆ t) (hts : t ⊆ closure s)
  {x : α} : IsLUB s x ↔ IsLUB t x

Full source

theorem isLUB_iff_of_subset_of_subset_closure {α : Type*} [TopologicalSpace α] [Preorder α]
    [ClosedIicTopology α] {s t : Set α} (hst : s ⊆ t) (hts : t ⊆ closure s) {x : α} :
    IsLUBIsLUB s x ↔ IsLUB t x :=
  isLUB_congr <| (upperBounds_closure (s := s) ▸ upperBounds_mono_set hts).antisymm <|
    upperBounds_mono_set hst

Least Upper Bound Preservation Under Closure Subset Relation

Informal description

Let $\alpha$ be a topological space with a preorder and the closed lower interval topology. For any subsets $s, t \subseteq \alpha$ such that $s \subseteq t$ and $t \subseteq \overline{s}$ (the closure of $s$), and for any $x \in \alpha$, the following are equivalent: 1. $x$ is the least upper bound of $s$, 2. $x$ is the least upper bound of $t$.

isGLB_iff_of_subset_of_subset_closure theorem

 {α : Type*} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {s t : Set α} (hst : s ⊆ t) (hts : t ⊆ closure s)
  {x : α} : IsGLB s x ↔ IsGLB t x

Full source

theorem isGLB_iff_of_subset_of_subset_closure {α : Type*} [TopologicalSpace α] [Preorder α]
    [ClosedIciTopology α] {s t : Set α} (hst : s ⊆ t) (hts : t ⊆ closure s) {x : α} :
    IsGLBIsGLB s x ↔ IsGLB t x :=
  isLUB_iff_of_subset_of_subset_closure (α := αᵒᵈ) hst hts

Greatest Lower Bound Preservation Under Closure Subset Relation in Closed Upper Interval Topology

Informal description

Let $\alpha$ be a topological space with a preorder and the closed upper interval topology. For any subsets $s, t \subseteq \alpha$ such that $s \subseteq t$ and $t \subseteq \overline{s}$ (the closure of $s$), and for any $x \in \alpha$, the following are equivalent: 1. $x$ is the greatest lower bound of $s$, 2. $x$ is the greatest lower bound of $t$.

Dense.isLUB_inter_iff theorem

 {α : Type*} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {s t : Set α} (hs : Dense s) (ht : IsOpen t)
  {x : α} : IsLUB (t ∩ s) x ↔ IsLUB t x

Full source

theorem Dense.isLUB_inter_iff {α : Type*} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α]
    {s t : Set α} (hs : Dense s) (ht : IsOpen t) {x : α} :
    IsLUBIsLUB (t ∩ s) x ↔ IsLUB t x :=
  isLUB_iff_of_subset_of_subset_closure (by simp) <| hs.open_subset_closure_inter ht

Least Upper Bound Equivalence for Dense-Open Intersection

Informal description

Let $\alpha$ be a topological space with a preorder and the closed lower interval topology. Let $s \subseteq \alpha$ be a dense subset and $t \subseteq \alpha$ be an open subset. For any $x \in \alpha$, the following are equivalent: 1. $x$ is the least upper bound of $t \cap s$, 2. $x$ is the least upper bound of $t$.

Dense.isGLB_inter_iff theorem

 {α : Type*} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {s t : Set α} (hs : Dense s) (ht : IsOpen t)
  {x : α} : IsGLB (t ∩ s) x ↔ IsGLB t x

Full source

theorem Dense.isGLB_inter_iff {α : Type*} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α]
    {s t : Set α} (hs : Dense s) (ht : IsOpen t) {x : α} :
    IsGLBIsGLB (t ∩ s) x ↔ IsGLB t x :=
  hs.isLUB_inter_iff (α := αᵒᵈ) ht

Greatest Lower Bound Equivalence for Dense-Open Intersection in Closed Upper Interval Topology

Informal description

Let $\alpha$ be a topological space with a preorder and the closed upper interval topology (where all intervals $[a, \infty)$ are closed). Let $s \subseteq \alpha$ be a dense subset and $t \subseteq \alpha$ be an open subset. For any $x \in \alpha$, the following are equivalent: 1. $x$ is the greatest lower bound of $t \cap s$, 2. $x$ is the greatest lower bound of $t$.

IsLUB.exists_seq_strictMono_tendsto_of_not_mem theorem

 {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

Full source

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 _

Existence of strictly increasing sequence converging to supremum from below

Informal description

Let $\alpha$ be a topological space with a preorder and countably generated neighborhoods. Let $t$ be a nonempty subset of $\alpha$ with least upper bound $x$, where $x \notin t$. Then there exists a strictly increasing sequence $(u_n)_{n \in \mathbb{N}}$ in $t$ such that $u_n < x$ for all $n$, and $u_n$ converges to $x$ as $n \to \infty$.

IsLUB.exists_seq_monotone_tendsto theorem

 {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

Full source

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⟩

Existence of monotone sequence converging to supremum from below

Informal description

Let $\alpha$ be a topological space with a preorder and countably generated neighborhoods. Let $t$ be a nonempty subset of $\alpha$ with least upper bound $x$. Then there exists a monotone sequence $(u_n)_{n \in \mathbb{N}}$ in $t$ such that $u_n \leq x$ for all $n$, and $u_n$ converges to $x$ as $n \to \infty$.

exists_seq_strictMono_tendsto' theorem

 {α : Type*} [LinearOrder α] [TopologicalSpace α] [DenselyOrdered α] [OrderTopology α] [FirstCountableTopology α]
  {x y : α} (hy : y < x) : ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)

Full source

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⟩

Existence of Strictly Increasing Sequence in $(y, x)$ Converging to $x$ in a Densely Ordered Space

Informal description

Let $\alpha$ be a linearly ordered topological space with a dense order and order topology, and assume $\alpha$ is first-countable. For any two elements $x, y \in \alpha$ such that $y < x$, there exists a strictly increasing sequence $(u_n)_{n \in \mathbb{N}}$ in $\alpha$ such that for all $n$, $u_n$ lies in the open interval $(y, x)$, and $u_n$ converges to $x$ as $n \to \infty$.

exists_seq_strictMono_tendsto theorem

 [DenselyOrdered α] [NoMinOrder α] [FirstCountableTopology α] (x : α) :
  ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n < x) ∧ Tendsto u atTop (𝓝 x)

Full source

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⟩

Existence of Strictly Increasing Sequence Converging to $x$ from Below in a Densely Ordered Space

Informal description

Let $\alpha$ be a densely ordered topological space with no minimal element and first-countable topology. For any element $x \in \alpha$, there exists a strictly increasing sequence $(u_n)_{n \in \mathbb{N}}$ in $\alpha$ such that $u_n < x$ for all $n$, and $u_n$ converges to $x$ as $n \to \infty$.

exists_seq_strictMono_tendsto_nhdsWithin theorem

 [DenselyOrdered α] [NoMinOrder α] [FirstCountableTopology α] (x : α) :
  ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n < x) ∧ Tendsto u atTop (𝓝[<] x)

Full source

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⟩

Existence of Strictly Increasing Sequence Converging to $x$ from Below in Left-Neighborhood Filter

Informal description

Let $\alpha$ be a densely ordered topological space with no minimal element and first-countable topology. For any element $x \in \alpha$, there exists a strictly increasing sequence $(u_n)_{n \in \mathbb{N}}$ in $\alpha$ such that $u_n < x$ for all $n$, and $u_n$ converges to $x$ within the left-neighborhood filter $\mathcal{N}[<] x$ as $n \to \infty$.

exists_seq_tendsto_sSup theorem

 {α : Type*} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [FirstCountableTopology α]
  {S : Set α} (hS : S.Nonempty) (hS' : BddAbove S) :
  ∃ u : ℕ → α, Monotone u ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ n, u n ∈ S

Full source

theorem exists_seq_tendsto_sSup {α : Type*} [ConditionallyCompleteLinearOrder α]
    [TopologicalSpace α] [OrderTopology α] [FirstCountableTopology α] {S : Set α} (hS : S.Nonempty)
    (hS' : BddAbove S) : ∃ u : ℕ → α, Monotone u ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ n, u n ∈ S := by
  rcases (isLUB_csSup hS hS').exists_seq_monotone_tendsto hS with ⟨u, hu⟩
  exact ⟨u, hu.1, hu.2.2⟩

Existence of Monotone Sequence Converging to Supremum in Conditionally Complete Linear Orders

Informal description

Let $\alpha$ be a conditionally complete linear order with the order topology and first-countable topology. For any nonempty subset $S \subseteq \alpha$ that is bounded above, there exists a monotone sequence $(u_n)_{n \in \mathbb{N}}$ in $S$ such that $u_n$ converges to the supremum $\sup S$ as $n \to \infty$.

Dense.exists_seq_strictMono_tendsto_of_lt theorem

 [DenselyOrdered α] [FirstCountableTopology α] {s : Set α} (hs : Dense s) {x y : α} (hy : y < x) :
  ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n ∈ (Ioo y x ∩ s)) ∧ Tendsto u atTop (𝓝 x)

Full source

theorem Dense.exists_seq_strictMono_tendsto_of_lt [DenselyOrdered α] [FirstCountableTopology α]
    {s : Set α} (hs : Dense s) {x y : α} (hy : y < x) :
    ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n ∈ (Ioo y x ∩ s)) ∧ Tendsto u atTop (𝓝 x) := by
  have hnonempty : (IooIoo y x ∩ s).Nonempty := by
    obtain ⟨z, hyz, hzx⟩ := hs.exists_between hy
    exact ⟨z, mem_inter hzx hyz⟩
  have hx : IsLUB (IooIoo y x ∩ s) x := hs.isLUB_inter_iff isOpen_Ioo |>.mpr <| isLUB_Ioo hy
  apply hx.exists_seq_strictMono_tendsto_of_not_mem (by aesop) hnonempty |>.imp
  aesop

Existence of strictly increasing sequence in dense subset converging to upper bound from within open interval

Informal description

Let $\alpha$ be a densely ordered topological space with first-countable topology, and let $s \subseteq \alpha$ be a dense subset. For any two elements $x, y \in \alpha$ with $y < x$, there exists a strictly increasing sequence $(u_n)_{n \in \mathbb{N}}$ in $\alpha$ such that: 1. For all $n$, $u_n$ belongs to both the open interval $(y, x)$ and the dense subset $s$, 2. The sequence $(u_n)$ converges to $x$ as $n \to \infty$.

Dense.exists_seq_strictMono_tendsto theorem

 [DenselyOrdered α] [NoMinOrder α] [FirstCountableTopology α] {s : Set α} (hs : Dense s) (x : α) :
  ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n ∈ (Iio x ∩ s)) ∧ Tendsto u atTop (𝓝 x)

Full source

theorem Dense.exists_seq_strictMono_tendsto [DenselyOrdered α] [NoMinOrder α]
    [FirstCountableTopology α] {s : Set α} (hs : Dense s) (x : α) :
    ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n ∈ (Iio x ∩ s)) ∧ Tendsto u atTop (𝓝 x) := by
  obtain ⟨y, hy⟩ := exists_lt x
  apply hs.exists_seq_strictMono_tendsto_of_lt (exists_lt x).choose_spec |>.imp
  aesop

Existence of strictly increasing sequence in dense subset converging to a point from below

Informal description

Let $\alpha$ be a densely ordered topological space with no minimal element and first-countable topology, and let $s \subseteq \alpha$ be a dense subset. For any element $x \in \alpha$, there exists a strictly increasing sequence $(u_n)_{n \in \mathbb{N}}$ in $\alpha$ such that: 1. For all $n$, $u_n$ belongs to both the left-infinite interval $(-\infty, x)$ and the dense subset $s$, 2. The sequence $(u_n)$ converges to $x$ as $n \to \infty$.

DenseRange.exists_seq_strictMono_tendsto_of_lt theorem

 {β : Type*} [LinearOrder β] [DenselyOrdered α] [FirstCountableTopology α] {f : β → α} {x y : α} (hf : DenseRange f)
  (hmono : Monotone f) (hlt : y < x) :
  ∃ u : ℕ → β, StrictMono u ∧ (∀ n, f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Full source

theorem DenseRange.exists_seq_strictMono_tendsto_of_lt {β : Type*} [LinearOrder β]
    [DenselyOrdered α] [FirstCountableTopology α] {f : β → α} {x y : α} (hf : DenseRange f)
    (hmono : Monotone f) (hlt : y < x) :
    ∃ u : ℕ → β, StrictMono u ∧ (∀ n, f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x) := by
  rcases Dense.exists_seq_strictMono_tendsto_of_lt hf hlt with ⟨u, hu, huyxf, hlim⟩
  have huyx (n : ℕ) : u n ∈ Ioo y x := (huyxf n).1
  have huf (n : ℕ) : u n ∈ range f := (huyxf n).2
  choose v hv using huf
  obtain rfl : f ∘ v = u := funext hv
  exact ⟨v, fun a b hlt ↦ hmono.reflect_lt <| hu hlt, huyx, hlim⟩

Existence of strictly increasing sequence in dense range converging to upper bound from within open interval

Informal description

Let $\alpha$ be a densely ordered topological space with first-countable topology, and let $\beta$ be a linearly ordered type. Given a monotone function $f \colon \beta \to \alpha$ with dense range, and two elements $x, y \in \alpha$ such that $y < x$, there exists a strictly increasing sequence $(u_n)_{n \in \mathbb{N}}$ in $\beta$ such that: 1. For all $n$, $f(u_n)$ belongs to the open interval $(y, x)$, 2. The sequence $(f(u_n))$ converges to $x$ as $n \to \infty$.

DenseRange.exists_seq_strictMono_tendsto theorem

 {β : Type*} [LinearOrder β] [DenselyOrdered α] [NoMinOrder α] [FirstCountableTopology α] {f : β → α}
  (hf : DenseRange f) (hmono : Monotone f) (x : α) :
  ∃ u : ℕ → β, StrictMono u ∧ (∀ n, f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Full source

theorem DenseRange.exists_seq_strictMono_tendsto {β : Type*} [LinearOrder β] [DenselyOrdered α]
    [NoMinOrder α] [FirstCountableTopology α] {f : β → α} (hf : DenseRange f) (hmono : Monotone f)
    (x : α):
    ∃ u : ℕ → β, StrictMono u ∧ (∀ n, f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x) := by
  rcases Dense.exists_seq_strictMono_tendsto hf x with ⟨u, hu, huxf, hlim⟩
  have hux (n : ℕ) : u n ∈ Iio x := (huxf n).1
  have huf (n : ℕ) : u n ∈ range f := (huxf n).2
  choose v hv using huf
  obtain rfl : f ∘ v = u := funext hv
  exact ⟨v, fun a b hlt ↦ hmono.reflect_lt <| hu hlt, hux, hlim⟩

Existence of strictly increasing sequence in dense range converging to a point from below

Informal description

Let $\alpha$ be a densely ordered topological space with no minimal element and first-countable topology, and let $\beta$ be a linearly ordered type. Given a monotone function $f \colon \beta \to \alpha$ with dense range and an element $x \in \alpha$, there exists a strictly increasing sequence $(u_n)_{n \in \mathbb{N}}$ in $\beta$ such that: 1. For all $n$, $f(u_n) \in (-\infty, x)$, 2. The sequence $(f(u_n))$ converges to $x$ as $n \to \infty$.

IsGLB.exists_seq_strictAnti_tendsto_of_not_mem theorem

 {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

Full source

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 (α := αᵒᵈ) htx not_mem ht

Existence of strictly decreasing sequence converging to infimum from above

Informal description

Let $\alpha$ be a topological space with a preorder and countably generated neighborhoods. Let $t$ be a nonempty subset of $\alpha$ with greatest lower bound $x$, where $x \notin t$. Then there exists a strictly decreasing sequence $(u_n)_{n \in \mathbb{N}}$ in $t$ such that $x < u_n$ for all $n$, and $u_n$ converges to $x$ as $n \to \infty$.

IsGLB.exists_seq_antitone_tendsto theorem

 {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

Full source

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 (α := αᵒᵈ) htx ht

Existence of antitone sequence converging to infimum from above

Informal description

Let $\alpha$ be a topological space with a preorder and countably generated neighborhoods. Let $t$ be a nonempty subset of $\alpha$ with greatest lower bound $x$. Then there exists an antitone sequence $(u_n)_{n \in \mathbb{N}}$ in $t$ such that $x \leq u_n$ for all $n$, and $u_n$ converges to $x$ as $n \to \infty$.

exists_seq_strictAnti_tendsto' theorem

 [DenselyOrdered α] [FirstCountableTopology α] {x y : α} (hy : x < y) :
  ∃ u : ℕ → α, StrictAnti u ∧ (∀ n, u n ∈ Ioo x y) ∧ Tendsto u atTop (𝓝 x)

Full source

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 using exists_seq_strictMono_tendsto' (α := αᵒᵈ) (OrderDual.toDual_lt_toDual.2 hy)

Existence of Strictly Decreasing Sequence in $(x, y)$ Converging to $x$ in a Densely Ordered Space

Informal description

Let $\alpha$ be a densely ordered topological space with first-countable topology, and let $x, y \in \alpha$ with $x < y$. Then there exists a strictly decreasing sequence $(u_n)_{n \in \mathbb{N}}$ in $\alpha$ such that for all $n$, $u_n$ lies in the open interval $(x, y)$, and $u_n$ converges to $x$ as $n \to \infty$.

exists_seq_strictAnti_tendsto theorem

 [DenselyOrdered α] [NoMaxOrder α] [FirstCountableTopology α] (x : α) :
  ∃ u : ℕ → α, StrictAnti u ∧ (∀ n, x < u n) ∧ Tendsto u atTop (𝓝 x)

Full source

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

Existence of Strictly Decreasing Sequence Converging to $x$ from Above in a Densely Ordered Space

Informal description

Let $\alpha$ be a densely ordered topological space with no maximal element and first-countable topology. For any element $x \in \alpha$, there exists a strictly decreasing sequence $(u_n)_{n \in \mathbb{N}}$ in $\alpha$ such that $x < u_n$ for all $n$, and $u_n$ converges to $x$ as $n \to \infty$.

exists_seq_strictAnti_tendsto_nhdsWithin theorem

 [DenselyOrdered α] [NoMaxOrder α] [FirstCountableTopology α] (x : α) :
  ∃ u : ℕ → α, StrictAnti u ∧ (∀ n, x < u n) ∧ Tendsto u atTop (𝓝[>] x)

Full source

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 (α := αᵒᵈ) _

Existence of Strictly Decreasing Sequence Converging to $x$ from Above in Right-Neighborhood Filter

Informal description

Let $\alpha$ be a densely ordered topological space with no maximal element and first-countable topology. For any element $x \in \alpha$, there exists a strictly decreasing sequence $(u_n)_{n \in \mathbb{N}}$ in $\alpha$ such that $x < u_n$ for all $n$, and $u_n$ converges to $x$ within the right-neighborhood filter $\mathcal{N}[>] x$ as $n \to \infty$.

exists_seq_strictAnti_strictMono_tendsto theorem

 [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)

Full source

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⟩

Existence of Strictly Decreasing and Increasing Sequences in $(x, y)$ Converging to $x$ and $y$ Respectively

Informal description

Let $\alpha$ be a densely ordered topological space with first-countable topology, and let $x, y \in \alpha$ with $x < y$. Then there exist sequences $(u_n)_{n \in \mathbb{N}}$ and $(v_n)_{n \in \mathbb{N}}$ in $\alpha$ such that: 1. $(u_n)$ is strictly decreasing, 2. $(v_n)$ is strictly increasing, 3. For all $k$, $u_k \in (x, y)$, 4. For all $l$, $v_l \in (x, y)$, 5. For all $k, l$, $u_k < v_l$, 6. $(u_n)$ converges to $x$ as $n \to \infty$, 7. $(v_n)$ converges to $y$ as $n \to \infty$.

exists_seq_tendsto_sInf theorem

 {α : Type*} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [FirstCountableTopology α]
  {S : Set α} (hS : S.Nonempty) (hS' : BddBelow S) :
  ∃ u : ℕ → α, Antitone u ∧ Tendsto u atTop (𝓝 (sInf S)) ∧ ∀ n, u n ∈ S

Full source

theorem exists_seq_tendsto_sInf {α : Type*} [ConditionallyCompleteLinearOrder α]
    [TopologicalSpace α] [OrderTopology α] [FirstCountableTopology α] {S : Set α} (hS : S.Nonempty)
    (hS' : BddBelow S) : ∃ u : ℕ → α, Antitone u ∧ Tendsto u atTop (𝓝 (sInf S)) ∧ ∀ n, u n ∈ S :=
  exists_seq_tendsto_sSup (α := αᵒᵈ) hS hS'

Existence of Antitone Sequence Converging to Infimum in Conditionally Complete Linear Orders

Informal description

Let $\alpha$ be a conditionally complete linear order with the order topology and first-countable topology. For any nonempty subset $S \subseteq \alpha$ that is bounded below, there exists an antitone sequence $(u_n)_{n \in \mathbb{N}}$ in $S$ such that $u_n$ converges to the infimum $\inf S$ as $n \to \infty$.

Dense.exists_seq_strictAnti_tendsto_of_lt theorem

 [DenselyOrdered α] [FirstCountableTopology α] {s : Set α} (hs : Dense s) {x y : α} (hy : x < y) :
  ∃ u : ℕ → α, StrictAnti u ∧ (∀ n, u n ∈ (Ioo x y ∩ s)) ∧ Tendsto u atTop (𝓝 x)

Full source

theorem Dense.exists_seq_strictAnti_tendsto_of_lt [DenselyOrdered α] [FirstCountableTopology α]
    {s : Set α} (hs : Dense s) {x y : α} (hy : x < y) :
    ∃ u : ℕ → α, StrictAnti u ∧ (∀ n, u n ∈ (Ioo x y ∩ s)) ∧ Tendsto u atTop (𝓝 x) := by
  simpa using hs.exists_seq_strictMono_tendsto_of_lt (α := αᵒᵈ) (OrderDual.toDual_lt_toDual.2 hy)

Existence of strictly decreasing sequence in dense subset converging to lower bound from within open interval

Informal description

Let $\alpha$ be a densely ordered topological space with first-countable topology, and let $s \subseteq \alpha$ be a dense subset. For any two elements $x, y \in \alpha$ with $x < y$, there exists a strictly decreasing sequence $(u_n)_{n \in \mathbb{N}}$ in $\alpha$ such that: 1. For all $n$, $u_n$ belongs to both the open interval $(x, y)$ and the dense subset $s$, 2. The sequence $(u_n)$ converges to $x$ as $n \to \infty$.

Dense.exists_seq_strictAnti_tendsto theorem

 [DenselyOrdered α] [NoMaxOrder α] [FirstCountableTopology α] {s : Set α} (hs : Dense s) (x : α) :
  ∃ u : ℕ → α, StrictAnti u ∧ (∀ n, u n ∈ (Ioi x ∩ s)) ∧ Tendsto u atTop (𝓝 x)

Full source

theorem Dense.exists_seq_strictAnti_tendsto [DenselyOrdered α] [NoMaxOrder α]
    [FirstCountableTopology α] {s : Set α} (hs : Dense s) (x : α) :
    ∃ u : ℕ → α, StrictAnti u ∧ (∀ n, u n ∈ (Ioi x ∩ s)) ∧ Tendsto u atTop (𝓝 x) :=
  hs.exists_seq_strictMono_tendsto (α := αᵒᵈ) x

Existence of strictly decreasing sequence in dense subset converging to a point from above

Informal description

Let $\alpha$ be a densely ordered topological space with no maximal element and first-countable topology, and let $s \subseteq \alpha$ be a dense subset. For any element $x \in \alpha$, there exists a strictly decreasing sequence $(u_n)_{n \in \mathbb{N}}$ in $\alpha$ such that: 1. For all $n$, $u_n$ belongs to both the right-infinite interval $(x, \infty)$ and the dense subset $s$, 2. The sequence $(u_n)$ converges to $x$ as $n \to \infty$.

DenseRange.exists_seq_strictAnti_tendsto_of_lt theorem

 {β : Type*} [LinearOrder β] [DenselyOrdered α] [FirstCountableTopology α] {f : β → α} {x y : α} (hf : DenseRange f)
  (hmono : Monotone f) (hlt : x < y) :
  ∃ u : ℕ → β, StrictAnti u ∧ (∀ n, f (u n) ∈ Ioo x y) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Full source

theorem DenseRange.exists_seq_strictAnti_tendsto_of_lt {β : Type*} [LinearOrder β]
    [DenselyOrdered α] [FirstCountableTopology α] {f : β → α} {x y : α} (hf : DenseRange f)
    (hmono : Monotone f) (hlt : x < y) :
    ∃ u : ℕ → β, StrictAnti u ∧ (∀ n, f (u n) ∈ Ioo x y) ∧ Tendsto (f ∘ u) atTop (𝓝 x) := by
  simpa using hf.exists_seq_strictMono_tendsto_of_lt (α := αᵒᵈ) (β := βᵒᵈ) hmono.dual
    (OrderDual.toDual_lt_toDual.2 hlt)

Existence of strictly decreasing sequence in dense range converging to lower bound from within open interval

Informal description

Let $\alpha$ be a densely ordered topological space with first-countable topology, and let $\beta$ be a linearly ordered type. Given a monotone function $f \colon \beta \to \alpha$ with dense range, and two elements $x, y \in \alpha$ such that $x < y$, there exists a strictly decreasing sequence $(u_n)_{n \in \mathbb{N}}$ in $\beta$ such that: 1. For all $n$, $f(u_n)$ belongs to the open interval $(x, y)$, 2. The sequence $(f(u_n))$ converges to $x$ as $n \to \infty$.

DenseRange.exists_seq_strictAnti_tendsto theorem

 {β : Type*} [LinearOrder β] [DenselyOrdered α] [NoMaxOrder α] [FirstCountableTopology α] {f : β → α}
  (hf : DenseRange f) (hmono : Monotone f) (x : α) :
  ∃ u : ℕ → β, StrictAnti u ∧ (∀ n, f (u n) ∈ Ioi x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Full source

theorem DenseRange.exists_seq_strictAnti_tendsto {β : Type*} [LinearOrder β] [DenselyOrdered α]
    [NoMaxOrder α] [FirstCountableTopology α] {f : β → α} (hf : DenseRange f) (hmono : Monotone f)
    (x : α):
    ∃ u : ℕ → β, StrictAnti u ∧ (∀ n, f (u n) ∈ Ioi x) ∧ Tendsto (f ∘ u) atTop (𝓝 x) :=
  hf.exists_seq_strictMono_tendsto (α := αᵒᵈ) (β := βᵒᵈ) hmono.dual x

Existence of strictly decreasing sequence in dense range converging to a point from above

Informal description

Let $\alpha$ be a densely ordered topological space with no maximal element and first-countable topology, and let $\beta$ be a linearly ordered type. Given a monotone function $f \colon \beta \to \alpha$ with dense range and an element $x \in \alpha$, there exists a strictly decreasing sequence $(u_n)_{n \in \mathbb{N}}$ in $\beta$ such that: 1. For all $n$, $f(u_n) \in (x, \infty)$, 2. The sequence $(f(u_n))$ converges to $x$ as $n \to \infty$.