doc-next-gen

Mathlib.Topology.Order.DenselyOrdered

Module docstring

{"# Order topology on a densely ordered set "}

closure_Ioi' theorem
{a : α} (h : (Ioi a).Nonempty) : closure (Ioi a) = Ici a
Full source 
/-- 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
Closure of Open Right-Infinite Interval Equals Closed Right-Infinite Interval
Informal description
For any element $a$ in a topological space $\alpha$ with an order topology, if the open interval $(a, \infty)$ is nonempty, then its closure is the closed interval $[a, \infty)$.
closure_Ioi theorem
(a : α) [NoMaxOrder α] : closure (Ioi a) = Ici a
Full source 
/-- 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
Closure of $(a, \infty)$ equals $[a, \infty)$ in order topology without maximal element
Informal description
For any element $a$ in a topological space $\alpha$ with an order topology and no maximal element, the closure of the open right-infinite interval $(a, \infty)$ is the closed right-infinite interval $[a, \infty)$.
closure_Iio' theorem
(h : (Iio a).Nonempty) : closure (Iio a) = Iic a
Full source 
/-- 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
Closure of Open Left-Infinite Interval Equals Closed Left-Infinite Interval
Informal description
For any element $a$ in a topological space $\alpha$ with an order topology, if the open left-infinite interval $(-\infty, a)$ is nonempty, then its closure is the closed left-infinite interval $(-\infty, a]$.
closure_Iio theorem
(a : α) [NoMinOrder α] : closure (Iio a) = Iic a
Full source 
/-- 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
Closure of $(-\infty, a)$ equals $(-\infty, a]$ in order topology without minimal element
Informal description
For any element $a$ in a topological space $\alpha$ with an order topology and no minimal element, the closure of the open left-infinite interval $(-\infty, a)$ is equal to the closed left-infinite interval $(-\infty, a]$.
closure_Ioo theorem
{a b : α} (hab : a ≠ b) : closure (Ioo a b) = Icc a b
Full source 
/-- 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
  · rcases 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_iff, 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 _
Closure of Open Interval in Densely Ordered Space: $\overline{(a,b)} = [a,b]$
Informal description
For any elements $a$ and $b$ in a densely ordered topological space $\alpha$ with $a \neq b$, the closure of the open interval $(a, b)$ is equal to the closed interval $[a, b]$.
closure_Ioc theorem
{a b : α} (hab : a ≠ b) : closure (Ioc a b) = Icc a b
Full source 
/-- 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]
Closure of Left-Open Right-Closed Interval in Densely Ordered Space: $\overline{(a,b]} = [a,b]$
Informal description
For any elements $a$ and $b$ in a densely ordered topological space $\alpha$ with $a \neq b$, the closure of the left-open right-closed interval $(a, b]$ is equal to the closed interval $[a, b]$.
closure_Ico theorem
{a b : α} (hab : a ≠ b) : closure (Ico a b) = Icc a b
Full source 
/-- 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]
Closure of Left-Closed Right-Open Interval in Densely Ordered Space: $\overline{[a,b)} = [a,b]$
Informal description
For any elements $a$ and $b$ in a densely ordered topological space $\alpha$ with $a \neq b$, the closure of the left-closed right-open interval $[a, b)$ is equal to the closed interval $[a, b]$.
interior_Ici' theorem
{a : α} (ha : (Iio a).Nonempty) : interior (Ici a) = Ioi a
Full source 
@[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]
Interior of Closed Right-Infinite Interval Equals Open Right-Infinite Interval Under Nonemptiness Condition
Informal description
For any element $a$ in a topological space $\alpha$ with an order topology, if the open left-infinite interval $(-\infty, a)$ is nonempty, then the interior of the closed right-infinite interval $[a, \infty)$ is the open right-infinite interval $(a, \infty)$. In other words, $\text{interior}([a, \infty)) = (a, \infty)$ under the given condition.
interior_Ici theorem
[NoMinOrder α] {a : α} : interior (Ici a) = Ioi a
Full source 
theorem interior_Ici [NoMinOrder α] {a : α} : interior (Ici a) = Ioi a :=
  interior_Ici' nonempty_Iio
Interior of Closed Right-Infinite Interval in No-Min-Order Space
Informal description
In a topological space $\alpha$ with an order topology and no minimal element, the interior of the closed right-infinite interval $[a, \infty)$ is equal to the open right-infinite interval $(a, \infty)$. That is, $\text{interior}([a, \infty)) = (a, \infty)$.
interior_Iic' theorem
{a : α} (ha : (Ioi a).Nonempty) : interior (Iic a) = Iio a
Full source 
@[simp]
theorem interior_Iic' {a : α} (ha : (Ioi a).Nonempty) : interior (Iic a) = Iio a :=
  interior_Ici' (α := αᵒᵈ) ha
Interior of Closed Left-Infinite Interval Equals Open Left-Infinite Interval Under Nonemptiness Condition
Informal description
For any element $a$ in a topological space $\alpha$ with an order topology, if the open right-infinite interval $(a, \infty)$ is nonempty, then the interior of the closed left-infinite interval $(-\infty, a]$ is the open left-infinite interval $(-\infty, a)$. In other words, $\text{interior}((-\infty, a]) = (-\infty, a)$ under the given condition.
interior_Iic theorem
[NoMaxOrder α] {a : α} : interior (Iic a) = Iio a
Full source 
theorem interior_Iic [NoMaxOrder α] {a : α} : interior (Iic a) = Iio a :=
  interior_Iic' nonempty_Ioi
Interior of Closed Left-Infinite Interval in No-Max-Order Space
Informal description
In a topological space $\alpha$ with an order topology and no maximal element, the interior of the closed left-infinite interval $(-\infty, a]$ is equal to the open left-infinite interval $(-\infty, a)$. That is, $\text{interior}((-\infty, a]) = (-\infty, a)$.
interior_Icc theorem
[NoMinOrder α] [NoMaxOrder α] {a b : α} : interior (Icc a b) = Ioo a b
Full source 
@[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]
Interior of Closed Interval Equals Open Interval in No-Min/Max-Order Space
Informal description
In a topological space $\alpha$ with an order topology and no minimal or maximal elements, the interior of the closed interval $[a, b]$ is equal to the open interval $(a, b)$. That is, $$\text{interior}([a, b]) = (a, b).$$
Icc_mem_nhds_iff theorem
[NoMinOrder α] [NoMaxOrder α] {a b x : α} : Icc a b ∈ 𝓝 x ↔ x ∈ Ioo a b
Full source 
@[simp]
theorem Icc_mem_nhds_iff [NoMinOrder α] [NoMaxOrder α] {a b x : α} :
    IccIcc a b ∈ 𝓝 xIcc a b ∈ 𝓝 x ↔ x ∈ Ioo a b := by
  rw [← interior_Icc, mem_interior_iff_mem_nhds]
Neighborhood Criterion for Closed Intervals in No-Min/Max-Order Space: $[a, b] \in \mathcal{N}(x) \iff x \in (a, b)$
Informal description
In a topological space $\alpha$ with an order topology and no minimal or maximal elements, the closed interval $[a, b]$ is a neighborhood of a point $x$ if and only if $x$ lies in the open interval $(a, b)$. That is, $$[a, b] \in \mathcal{N}(x) \iff x \in (a, b).$$
interior_Ico theorem
[NoMinOrder α] {a b : α} : interior (Ico a b) = Ioo a b
Full source 
@[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]
Interior of $[a, b)$ Equals $(a, b)$ in No-Min-Order Space
Informal description
In a topological space $\alpha$ with an order topology and no minimal element, the interior of the left-closed right-open interval $[a, b)$ is equal to the open interval $(a, b)$. That is, $$\text{interior}([a, b)) = (a, b).$$
Ico_mem_nhds_iff theorem
[NoMinOrder α] {a b x : α} : Ico a b ∈ 𝓝 x ↔ x ∈ Ioo a b
Full source 
@[simp]
theorem Ico_mem_nhds_iff [NoMinOrder α] {a b x : α} : IcoIco a b ∈ 𝓝 xIco a b ∈ 𝓝 x ↔ x ∈ Ioo a b := by
  rw [← interior_Ico, mem_interior_iff_mem_nhds]
Neighborhood Criterion for $[a, b)$ in No-Min-Order Space: $[a, b) \in \mathcal{N}(x) \iff x \in (a, b)$
Informal description
In a topological space $\alpha$ with an order topology and no minimal element, the left-closed right-open interval $[a, b)$ is a neighborhood of a point $x$ if and only if $x$ lies in the open interval $(a, b)$. That is, $$[a, b) \in \mathcal{N}(x) \iff x \in (a, b).$$
interior_Ioc theorem
[NoMaxOrder α] {a b : α} : interior (Ioc a b) = Ioo a b
Full source 
@[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]
Interior of $(a, b]$ equals $(a, b)$ in no-max-order space
Informal description
In a topological space $\alpha$ with an order topology and no maximal element, the interior of the left-open right-closed interval $(a, b]$ is equal to the open interval $(a, b)$. That is, $$\text{interior}((a, b]) = (a, b).$$
Ioc_mem_nhds_iff theorem
[NoMaxOrder α] {a b x : α} : Ioc a b ∈ 𝓝 x ↔ x ∈ Ioo a b
Full source 
@[simp]
theorem Ioc_mem_nhds_iff [NoMaxOrder α] {a b x : α} : IocIoc a b ∈ 𝓝 xIoc a b ∈ 𝓝 x ↔ x ∈ Ioo a b := by
  rw [← interior_Ioc, mem_interior_iff_mem_nhds]
Neighborhood Criterion for $(a, b]$ in No-Max-Order Space: $(a, b] \in \mathcal{N}(x) \iff x \in (a, b)$
Informal description
In a topological space $\alpha$ with an order topology and no maximal element, the left-open right-closed interval $(a, b]$ is a neighborhood of a point $x$ if and only if $x$ lies in the open interval $(a, b)$. That is, $$(a, b] \in \mathcal{N}(x) \iff x \in (a, b).$$
closure_interior_Icc theorem
{a b : α} (h : a ≠ b) : closure (interior (Icc a b)) = Icc a b
Full source 
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)
Closure of Interior of Closed Interval Equals Closed Interval in Densely Ordered Space
Informal description
For any elements $a$ and $b$ in a densely ordered topological space $\alpha$ with $a \neq b$, the closure of the interior of the closed interval $[a, b]$ equals $[a, b]$, i.e., $\overline{\text{int}([a, b])} = [a, b]$.
Ioc_subset_closure_interior theorem
(a b : α) : Ioc a b ⊆ closure (interior (Ioc a b))
Full source 
theorem Ioc_subset_closure_interior (a b : α) : IocIoc 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)
Inclusion of $(a, b]$ in the Closure of its Interior
Informal description
For any elements $a$ and $b$ in a topological space $\alpha$ with an order topology, the left-open right-closed interval $(a, b]$ is contained in the closure of the interior of $(a, b]$. In other words, $Ioc(a, b) \subseteq \overline{\text{int}(Ioc(a, b))}$.
Ico_subset_closure_interior theorem
(a b : α) : Ico a b ⊆ closure (interior (Ico a b))
Full source 
theorem Ico_subset_closure_interior (a b : α) : IcoIco a b ⊆ closure (interior (Ico a b)) := by
  simpa only [Ioc_toDual] using
    Ioc_subset_closure_interior (OrderDual.toDual b) (OrderDual.toDual a)
Inclusion of $[a, b)$ in the Closure of its Interior in Order Topology
Informal description
For any elements $a$ and $b$ in a topological space $\alpha$ with an order topology, the left-closed right-open interval $[a, b)$ is contained in the closure of the interior of $[a, b)$. In other words, $[a, b) \subseteq \overline{\text{int}([a, b))}$.
frontier_Ici' theorem
{a : α} (ha : (Iio a).Nonempty) : frontier (Ici a) = { a }
Full source 
@[simp]
theorem frontier_Ici' {a : α} (ha : (Iio a).Nonempty) : frontier (Ici a) = {a} := by
  simp [frontier, ha]
Frontier of Closed Right-Infinite Interval Equals Singleton Under Nonemptiness Condition
Informal description
For any element $a$ in a topological space $\alpha$ with an order topology, if the open left-infinite interval $(-\infty, a)$ is nonempty, then the frontier (boundary) of the closed right-infinite interval $[a, \infty)$ is the singleton set $\{a\}$. In other words, $\text{frontier}([a, \infty)) = \{a\}$ under the given condition.
frontier_Ici theorem
[NoMinOrder α] {a : α} : frontier (Ici a) = { a }
Full source 
theorem frontier_Ici [NoMinOrder α] {a : α} : frontier (Ici a) = {a} :=
  frontier_Ici' nonempty_Iio
Frontier of $[a, \infty)$ is $\{a\}$ in order topology without minimal element
Informal description
In a topological space $\alpha$ with an order topology and no minimal element, the frontier (boundary) of the closed right-infinite interval $[a, \infty)$ is the singleton set $\{a\}$, i.e., $\text{frontier}([a, \infty)) = \{a\}$.
frontier_Iic' theorem
{a : α} (ha : (Ioi a).Nonempty) : frontier (Iic a) = { a }
Full source 
@[simp]
theorem frontier_Iic' {a : α} (ha : (Ioi a).Nonempty) : frontier (Iic a) = {a} := by
  simp [frontier, ha]
Frontier of Closed Left-Infinite Interval Equals Singleton Under Nonemptiness Condition
Informal description
For any element $a$ in a topological space $\alpha$ with an order topology, if the open right-infinite interval $(a, \infty)$ is nonempty, then the frontier (boundary) of the closed left-infinite interval $(-\infty, a]$ is the singleton set $\{a\}$. In other words, $\text{frontier}((-\infty, a]) = \{a\}$ under the given condition.
frontier_Iic theorem
[NoMaxOrder α] {a : α} : frontier (Iic a) = { a }
Full source 
theorem frontier_Iic [NoMaxOrder α] {a : α} : frontier (Iic a) = {a} :=
  frontier_Iic' nonempty_Ioi
Frontier of $(-\infty, a]$ is $\{a\}$ in order topology without maximal element
Informal description
In a topological space $\alpha$ with an order topology and no maximal element, the frontier (boundary) of the closed left-infinite interval $(-\infty, a]$ is the singleton set $\{a\}$, i.e., $\text{frontier}((-\infty, a]) = \{a\}$.
frontier_Ioi' theorem
{a : α} (ha : (Ioi a).Nonempty) : frontier (Ioi a) = { a }
Full source 
@[simp]
theorem frontier_Ioi' {a : α} (ha : (Ioi a).Nonempty) : frontier (Ioi a) = {a} := by
  simp [frontier, closure_Ioi' ha, Iic_diff_Iio, Icc_self]
Frontier of Open Right-Infinite Interval is Singleton $\{a\}$
Informal description
For any element $a$ in a topological space $\alpha$ with an order topology, if the open interval $(a, \infty)$ is nonempty, then its frontier (boundary) is the singleton set $\{a\}$.
frontier_Ioi theorem
[NoMaxOrder α] {a : α} : frontier (Ioi a) = { a }
Full source 
theorem frontier_Ioi [NoMaxOrder α] {a : α} : frontier (Ioi a) = {a} :=
  frontier_Ioi' nonempty_Ioi
Frontier of $(a, \infty)$ is $\{a\}$ in order topology without maximal element
Informal description
In a topological space $\alpha$ with an order topology and no maximal element, the frontier (boundary) of the open right-infinite interval $(a, \infty)$ is the singleton set $\{a\}$.
frontier_Iio' theorem
{a : α} (ha : (Iio a).Nonempty) : frontier (Iio a) = { a }
Full source 
@[simp]
theorem frontier_Iio' {a : α} (ha : (Iio a).Nonempty) : frontier (Iio a) = {a} := by
  simp [frontier, closure_Iio' ha, Iic_diff_Iio, Icc_self]
Frontier of Open Left-Infinite Interval is Singleton $\{a\}$
Informal description
For any element $a$ in a topological space $\alpha$ with an order topology, if the open left-infinite interval $(-\infty, a)$ is nonempty, then its frontier (boundary) is the singleton set $\{a\}$.
frontier_Iio theorem
[NoMinOrder α] {a : α} : frontier (Iio a) = { a }
Full source 
theorem frontier_Iio [NoMinOrder α] {a : α} : frontier (Iio a) = {a} :=
  frontier_Iio' nonempty_Iio
Frontier of $(-\infty, a)$ is $\{a\}$ in order topology without minimal element
Informal description
In a topological space $\alpha$ with an order topology and no minimal element, the frontier (boundary) of the open left-infinite interval $(-\infty, a)$ is the singleton set $\{a\}$.
frontier_Icc theorem
[NoMinOrder α] [NoMaxOrder α] {a b : α} (h : a ≤ b) : frontier (Icc a b) = { a, b }
Full source 
@[simp]
theorem frontier_Icc [NoMinOrder α] [NoMaxOrder α] {a b : α} (h : a ≤ b) :
    frontier (Icc a b) = {a, b} := by simp [frontier, h, Icc_diff_Ioo_same]
Frontier of Closed Interval Equals Endpoints in Order Topology without Extremes
Informal description
In a topological space $\alpha$ with an order topology and no minimal or maximal elements, for any elements $a$ and $b$ with $a \leq b$, the frontier (boundary) of the closed interval $[a, b]$ is the set $\{a, b\}$. That is, $$\partial([a, b]) = \{a, b\}.$$
frontier_Ioo theorem
{a b : α} (h : a < b) : frontier (Ioo a b) = { a, b }
Full source 
@[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]
Frontier of Open Interval Equals Endpoints: $\partial(a, b) = \{a, b\}$
Informal description
For any elements $a$ and $b$ in a topological space $\alpha$ with $a < b$, the frontier of the open interval $(a, b)$ is the set $\{a, b\}$.
frontier_Ico theorem
[NoMinOrder α] {a b : α} (h : a < b) : frontier (Ico a b) = { a, b }
Full source 
@[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]
Frontier of $[a, b)$ Equals $\{a, b\}$ in No-Min-Order Space
Informal description
In a topological space $\alpha$ with an order topology and no minimal element, for any elements $a$ and $b$ with $a < b$, the frontier of the left-closed right-open interval $[a, b)$ is the set $\{a, b\}$. That is, $$\partial([a, b)) = \{a, b\}.$$
frontier_Ioc theorem
[NoMaxOrder α] {a b : α} (h : a < b) : frontier (Ioc a b) = { a, b }
Full source 
@[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]
Frontier of $(a, b]$ equals $\{a, b\}$ in no-max-order space
Informal description
In a topological space $\alpha$ with an order topology and no maximal element, for any elements $a$ and $b$ with $a < b$, the frontier of the left-open right-closed interval $(a, b]$ is the set $\{a, b\}$. That is, $$\partial((a, b]) = \{a, b\}.$$
nhdsWithin_Ioi_neBot' theorem
{a b : α} (H₁ : (Ioi a).Nonempty) (H₂ : a ≤ b) : NeBot (𝓝[Ioi a] b)
Full source 
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₁]
Non-triviality of Neighborhood Filter within Open Right-Infinite Interval
Informal description
For any elements $a$ and $b$ in a topological space $\alpha$ with an order topology, if the open interval $(a, \infty)$ is nonempty and $a \leq b$, then the neighborhood filter of $b$ within $(a, \infty)$ is non-trivial (i.e., it does not contain the empty set).
nhdsWithin_Ioi_neBot theorem
[NoMaxOrder α] {a b : α} (H : a ≤ b) : NeBot (𝓝[Ioi a] b)
Full source 
theorem nhdsWithin_Ioi_neBot [NoMaxOrder α] {a b : α} (H : a ≤ b) : NeBot (𝓝[Ioi a] b) :=
  nhdsWithin_Ioi_neBot' nonempty_Ioi H
Non-triviality of Neighborhood Filter in Right-Infinite Interval for NoMaxOrder
Informal description
Let $\alpha$ be a preorder with no maximal element (i.e., for every $a \in \alpha$ there exists $b \in \alpha$ such that $a < b$). For any elements $a, b \in \alpha$ with $a \leq b$, the neighborhood filter of $b$ within the open right-infinite interval $(a, \infty)$ is non-trivial (i.e., it does not contain the empty set).
nhdsGT_neBot_of_exists_gt theorem
{a : α} (H : ∃ b, a < b) : NeBot (𝓝[>] a)
Full source 
theorem nhdsGT_neBot_of_exists_gt {a : α} (H : ∃ b, a < b) : NeBot (𝓝[>] a) :=
  nhdsWithin_Ioi_neBot' H (le_refl a)
Non-triviality of Right Neighborhood Filter for Elements with Successors
Informal description
For any element $a$ in a topological space $\alpha$ with an order topology, if there exists an element $b$ such that $a < b$, then the neighborhood filter of $a$ restricted to the open right-infinite interval $(a, \infty)$ is non-trivial (i.e., it does not contain the empty set).
nhdsGT_neBot instance
[NoMaxOrder α] (a : α) : NeBot (𝓝[>] a)
Full source 
instance nhdsGT_neBot [NoMaxOrder α] (a : α) : NeBot (𝓝[>] a) := nhdsWithin_Ioi_neBot le_rfl
Non-triviality of Right Neighborhood Filter in NoMaxOrder
Informal description
For any element $a$ in a preorder $\alpha$ with no maximal element, the neighborhood filter of $a$ restricted to the open right-infinite interval $(a, \infty)$ is non-trivial (i.e., it does not contain the empty set).
nhdsWithin_Ioi_self_neBot theorem
[NoMaxOrder α] (a : α) : NeBot (𝓝[>] a)
Full source 
@[deprecated nhdsGT_neBot (since := "2024-12-22")]
theorem nhdsWithin_Ioi_self_neBot [NoMaxOrder α] (a : α) : NeBot (𝓝[>] a) := nhdsGT_neBot a
Non-triviality of Right Neighborhood Filter in No-Max-Order Spaces
Informal description
For any element $a$ in a preorder $\alpha$ with no maximal element, the neighborhood filter of $a$ restricted to the open right-infinite interval $(a, \infty)$ is non-trivial (i.e., it does not contain the empty set).
nhdsWithin_Iio_neBot' theorem
{b c : α} (H₁ : (Iio c).Nonempty) (H₂ : b ≤ c) : NeBot (𝓝[Iio c] b)
Full source 
theorem nhdsWithin_Iio_neBot' {b c : α} (H₁ : (Iio c).Nonempty) (H₂ : b ≤ c) :
    NeBot (𝓝[Iio c] b) :=
  mem_closure_iff_nhdsWithin_neBot.1 <| by rwa [closure_Iio' H₁]
Non-triviality of Left Neighborhood Filter in Open Left-Infinite Interval
Informal description
For any elements $b$ and $c$ in a topological space $\alpha$ with an order topology, if the open left-infinite interval $(-\infty, c)$ is nonempty and $b \leq c$, then the neighborhood filter of $b$ restricted to $(-\infty, c)$ is non-trivial (i.e., it does not contain the empty set).
nhdsWithin_Iio_neBot theorem
[NoMinOrder α] {a b : α} (H : a ≤ b) : NeBot (𝓝[Iio b] a)
Full source 
theorem nhdsWithin_Iio_neBot [NoMinOrder α] {a b : α} (H : a ≤ b) : NeBot (𝓝[Iio b] a) :=
  nhdsWithin_Iio_neBot' nonempty_Iio H
Non-triviality of Left Neighborhood Filter in Open Left-Infinite Interval under No-Min-Order Condition
Informal description
In a topological space $\alpha$ with an order topology and no minimal element, for any elements $a$ and $b$ such that $a \leq b$, the neighborhood filter of $a$ restricted to the open left-infinite interval $(-\infty, b)$ is non-trivial (i.e., it does not contain the empty set).
nhdsWithin_Iio_self_neBot' theorem
{b : α} (H : (Iio b).Nonempty) : NeBot (𝓝[<] b)
Full source 
theorem nhdsWithin_Iio_self_neBot' {b : α} (H : (Iio b).Nonempty) : NeBot (𝓝[<] b) :=
  nhdsWithin_Iio_neBot' H (le_refl b)
Non-triviality of Left Neighborhood Filter at Point in Open Left-Infinite Interval
Informal description
For any element $b$ in a topological space $\alpha$ with an order topology, if the open left-infinite interval $(-\infty, b)$ is nonempty, then the neighborhood filter of $b$ restricted to $(-\infty, b)$ is non-trivial (i.e., it does not contain the empty set).
nhdsLT_neBot instance
[NoMinOrder α] (a : α) : NeBot (𝓝[<] a)
Full source 
instance nhdsLT_neBot [NoMinOrder α] (a : α) : NeBot (𝓝[<] a) := nhdsWithin_Iio_neBot (le_refl a)
Non-triviality of Left Neighborhood Filter in No-Min-Order Spaces
Informal description
In a topological space $\alpha$ with an order topology and no minimal element, for any element $a \in \alpha$, the neighborhood filter of $a$ restricted to the set of elements less than $a$ is non-trivial (i.e., it does not contain the empty set).
nhdsWithin_Iio_self_neBot theorem
[NoMinOrder α] (a : α) : NeBot (𝓝[<] a)
Full source 
@[deprecated nhdsLT_neBot (since := "2024-12-22")]
theorem nhdsWithin_Iio_self_neBot [NoMinOrder α] (a : α) : NeBot (𝓝[<] a) := nhdsLT_neBot a
Non-triviality of Left Neighborhood Filter in Spaces Without Minimal Elements
Informal description
Let $\alpha$ be a topological space with an order topology and no minimal element. For any element $a \in \alpha$, the neighborhood filter of $a$ restricted to the set $\{x \mid x < a\}$ is non-trivial (i.e., it does not contain the empty set).
right_nhdsWithin_Ico_neBot theorem
{a b : α} (H : a < b) : NeBot (𝓝[Ico a b] b)
Full source 
theorem right_nhdsWithin_Ico_neBot {a b : α} (H : a < b) : NeBot (𝓝[Ico a b] b) :=
  (isLUB_Ico H).nhdsWithin_neBot (nonempty_Ico.2 H)
Non-triviality of Right Neighborhood Filter in $[a, b)$ Interval
Informal description
Let $\alpha$ be a topological space with an order topology, and let $a, b \in \alpha$ with $a < b$. Then the neighborhood filter of $b$ within the interval $[a, b)$ is non-trivial (i.e., contains more than just the empty set).
left_nhdsWithin_Ioc_neBot theorem
{a b : α} (H : a < b) : NeBot (𝓝[Ioc a b] a)
Full source 
theorem left_nhdsWithin_Ioc_neBot {a b : α} (H : a < b) : NeBot (𝓝[Ioc a b] a) :=
  (isGLB_Ioc H).nhdsWithin_neBot (nonempty_Ioc.2 H)
Non-triviality of Left-Neighborhood Filter in $(a, b]$ Interval
Informal description
Let $\alpha$ be a topological space with an order topology, and let $a, b \in \alpha$ with $a < b$. Then the neighborhood filter of $a$ within the left-open right-closed interval $(a, b]$ is non-trivial (i.e., contains more than just the empty set).
left_nhdsWithin_Ioo_neBot theorem
{a b : α} (H : a < b) : NeBot (𝓝[Ioo a b] a)
Full source 
theorem left_nhdsWithin_Ioo_neBot {a b : α} (H : a < b) : NeBot (𝓝[Ioo a b] a) :=
  (isGLB_Ioo H).nhdsWithin_neBot (nonempty_Ioo.2 H)
Non-triviality of Left-Neighborhood Filter in Open Interval $(a, b)$
Informal description
Let $\alpha$ be a topological space with an order topology, and let $a, b \in \alpha$ with $a < b$. Then the neighborhood filter of $a$ within the open interval $(a, b)$ is non-trivial (i.e., contains more than just the empty set).
right_nhdsWithin_Ioo_neBot theorem
{a b : α} (H : a < b) : NeBot (𝓝[Ioo a b] b)
Full source 
theorem right_nhdsWithin_Ioo_neBot {a b : α} (H : a < b) : NeBot (𝓝[Ioo a b] b) :=
  (isLUB_Ioo H).nhdsWithin_neBot (nonempty_Ioo.2 H)
Non-triviality of Right-Neighborhood Filter in Open Interval $(a, b)$
Informal description
Let $\alpha$ be a topological space with an order topology, and let $a, b \in \alpha$ with $a < b$. Then the neighborhood filter of $b$ within the open interval $(a, b)$ is non-trivial (i.e., contains more than just the empty set).
comap_coe_nhdsLT_of_Ioo_subset theorem
(hb : s ⊆ Iio b) (hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s) : comap ((↑) : s → α) (𝓝[<] b) = atTop
Full source 
theorem comap_coe_nhdsLT_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 : IooIoo x b ⊆ t⟩ :=
      (mem_nhdsLT_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_nhdsLT (hb x.2), fun z hz => hx _ hz.1.le⟩
Pullback of Left-Neighborhood Filter via Open Interval Inclusion
Informal description
Let $\alpha$ be a topological space with an order topology, and let $s$ be a subset of $\alpha$ such that $s \subseteq (-\infty, b)$. If $s$ is nonempty, suppose there exists $a < b$ such that the open interval $(a, b)$ is contained in $s$. Then the pullback of the left-neighborhood filter $\mathcal{N}_{[<]}(b)$ under the inclusion map $s \hookrightarrow \alpha$ is equal to the filter at infinity on $s$.
comap_coe_nhdsGT_of_Ioo_subset theorem
(ha : s ⊆ Ioi a) (hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s) : comap ((↑) : s → α) (𝓝[>] a) = atBot
Full source 
theorem comap_coe_nhdsGT_of_Ioo_subset (ha : s ⊆ Ioi a) (hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s) :
    comap ((↑) : s → α) (𝓝[>] a) = atBot := by
  apply comap_coe_nhdsLT_of_Ioo_subset (show ofDualofDual ⁻¹' sofDual ⁻¹' s ⊆ Iio (toDual a) from ha)
  simp only [OrderDual.exists, Ioo_toDual]
  exact hs
Pullback of Right-Neighborhood Filter via Open Interval Inclusion Yields Filter at Negative Infinity
Informal description
Let $\alpha$ be a topological space with an order topology, and let $s$ be a subset of $\alpha$ such that $s \subseteq (a, \infty)$. If $s$ is nonempty, suppose there exists $b > a$ such that the open interval $(a, b)$ is contained in $s$. Then the pullback of the right-neighborhood filter $\mathcal{N}_{[>]}(a)$ under the inclusion map $s \hookrightarrow \alpha$ is equal to the filter at negative infinity on $s$.
map_coe_atTop_of_Ioo_subset theorem
(hb : s ⊆ Iio b) (hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s) : map ((↑) : s → α) atTop = 𝓝[<] b
Full source 
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_nhdsLT_of_Ioo_subset hb fun _ => hs a ha, map_comap_of_mem]
    rw [Subtype.range_val]
    exact (mem_nhdsLT_iff_exists_Ioo_subset' ha).2 (hs a ha)
Pushforward of Filter at Infinity to Left-Neighborhood Filter via Open Interval Inclusion
Informal description
Let $\alpha$ be a topological space with an order topology, and let $s$ be a subset of $\alpha$ such that $s \subseteq (-\infty, b)$. Suppose that for every $a' < b$, there exists $a < b$ such that the open interval $(a, b)$ is contained in $s$. Then the pushforward of the filter at infinity on $s$ under the inclusion map $s \hookrightarrow \alpha$ is equal to the left-neighborhood filter $\mathcal{N}_{[<]}(b)$.
map_coe_atBot_of_Ioo_subset theorem
(ha : s ⊆ Ioi a) (hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s) : map ((↑) : s → α) atBot = 𝓝[>] a
Full source 
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 ofDualofDual ⁻¹' sofDual ⁻¹' s ⊆ Iio (toDual a) from ha)
    fun b' hb' => ?_ :)
  simpa using hs b' hb'
Pushforward of Filter at Negative Infinity to Right-Neighborhood Filter via Open Interval Inclusion
Informal description
Let $\alpha$ be a topological space with an order topology, and let $s$ be a subset of $\alpha$ such that $s \subseteq (a, \infty)$. Suppose that for every $b' > a$, there exists $b > a$ such that the open interval $(a, b) \subseteq s$. Then the pushforward of the filter at negative infinity on $s$ under the inclusion map $s \hookrightarrow \alpha$ is equal to the right-neighborhood filter $\mathcal{N}_{[>]}(a)$.
comap_coe_Ioo_nhdsLT theorem
(a b : α) : comap ((↑) : Ioo a b → α) (𝓝[<] b) = atTop
Full source 
/-- 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_nhdsLT (a b : α) : comap ((↑) : Ioo a b → α) (𝓝[<] b) = atTop :=
  comap_coe_nhdsLT_of_Ioo_subset Ioo_subset_Iio_self fun h => ⟨a, nonempty_Ioo.1 h, Subset.refl _⟩
Pullback of Left-Neighborhood Filter via Open Interval Inclusion Yields Filter at Infinity
Informal description
Let $\alpha$ be a topological space with an order topology, and let $(a, b)$ be an open interval in $\alpha$. The pullback of the left-neighborhood filter $\mathcal{N}_{[<]}(b)$ under the inclusion map $(a, b) \hookrightarrow \alpha$ is equal to the filter at infinity on $(a, b)$.
comap_coe_Ioo_nhdsGT theorem
(a b : α) : comap ((↑) : Ioo a b → α) (𝓝[>] a) = atBot
Full source 
/-- 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_nhdsGT (a b : α) : comap ((↑) : Ioo a b → α) (𝓝[>] a) = atBot :=
  comap_coe_nhdsGT_of_Ioo_subset Ioo_subset_Ioi_self fun h => ⟨b, nonempty_Ioo.1 h, Subset.refl _⟩
Pullback of Right-Neighborhood Filter via Open Interval Inclusion Yields Filter at Negative Infinity
Informal description
Let $\alpha$ be a topological space with an order topology, and let $(a, b)$ be an open interval in $\alpha$. The pullback of the right-neighborhood filter $\mathcal{N}_{[>]}(a)$ under the inclusion map $(a, b) \hookrightarrow \alpha$ is equal to the filter at negative infinity on $(a, b)$.
comap_coe_Ioi_nhdsGT theorem
(a : α) : comap ((↑) : Ioi a → α) (𝓝[>] a) = atBot
Full source 
theorem comap_coe_Ioi_nhdsGT (a : α) : comap ((↑) : Ioi a → α) (𝓝[>] a) = atBot :=
  comap_coe_nhdsGT_of_Ioo_subset (Subset.refl _) fun ⟨x, hx⟩ => ⟨x, hx, Ioo_subset_Ioi_self⟩
Pullback of Right-Neighborhood Filter via Right-Infinite Inclusion Yields Filter at Negative Infinity
Informal description
Let $\alpha$ be a topological space with an order topology. For any element $a \in \alpha$, the pullback of the right-neighborhood filter $\mathcal{N}_{[>]}(a)$ under the inclusion map $(a, \infty) \hookrightarrow \alpha$ is equal to the filter at negative infinity on $(a, \infty)$.
comap_coe_Iio_nhdsLT theorem
(a : α) : comap ((↑) : Iio a → α) (𝓝[<] a) = atTop
Full source 
theorem comap_coe_Iio_nhdsLT (a : α) : comap ((↑) : Iio a → α) (𝓝[<] a) = atTop :=
  comap_coe_Ioi_nhdsGT (α := αᵒᵈ) a
Pullback of Left-Neighborhood Filter via Left-Infinite Inclusion Yields Filter at Positive Infinity
Informal description
Let $\alpha$ be a topological space with an order topology. For any element $a \in \alpha$, the pullback of the left-neighborhood filter $\mathcal{N}_{[<]}(a)$ under the inclusion map $(-\infty, a) \hookrightarrow \alpha$ is equal to the filter at positive infinity on $(-\infty, a)$.
map_coe_Ioo_atTop theorem
{a b : α} (h : a < b) : map ((↑) : Ioo a b → α) atTop = 𝓝[<] b
Full source 
@[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 _⟩
Pushforward of Filter at Infinity on $(a, b)$ to Left-Neighborhood Filter at $b$
Informal description
Let $\alpha$ be a preordered topological space with the order topology, and let $a, b \in \alpha$ with $a < b$. Then the pushforward of the filter at infinity on the open interval $(a, b)$ under the inclusion map $(a, b) \hookrightarrow \alpha$ is equal to the left-neighborhood filter $\mathcal{N}_{[<]}(b)$ at $b$.
map_coe_Ioo_atBot theorem
{a b : α} (h : a < b) : map ((↑) : Ioo a b → α) atBot = 𝓝[>] a
Full source 
@[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 _⟩
Pushforward of Filter at Negative Infinity on $(a, b)$ to Right-Neighborhood Filter at $a$
Informal description
Let $\alpha$ be a preordered topological space with the order topology, and let $a, b \in \alpha$ with $a < b$. Then the pushforward of the filter at negative infinity on the open interval $(a, b)$ under the inclusion map $(a, b) \hookrightarrow \alpha$ is equal to the right-neighborhood filter $\mathcal{N}_{[>]}(a)$ at $a$.
map_coe_Ioi_atBot theorem
(a : α) : map ((↑) : Ioi a → α) atBot = 𝓝[>] a
Full source 
@[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⟩
Pushforward of Filter at Negative Infinity on $(a, \infty)$ to Right-Neighborhood Filter at $a$
Informal description
Let $\alpha$ be a preordered topological space with the order topology. For any element $a \in \alpha$, the pushforward of the filter at negative infinity on the left-open right-infinite interval $(a, \infty)$ under the inclusion map $(a, \infty) \hookrightarrow \alpha$ is equal to the right-neighborhood filter $\mathcal{N}_{[>]}(a)$ at $a$.
map_coe_Iio_atTop theorem
(a : α) : map ((↑) : Iio a → α) atTop = 𝓝[<] a
Full source 
@[simp]
theorem map_coe_Iio_atTop (a : α) : map ((↑) : Iio a → α) atTop = 𝓝[<] a :=
  map_coe_Ioi_atBot (α := αᵒᵈ) _
Pushforward of Filter at Infinity on $(-\infty, a)$ to Left-Neighborhood Filter at $a$
Informal description
Let $\alpha$ be a preordered topological space with the order topology. For any element $a \in \alpha$, the pushforward of the filter at positive infinity on the right-infinite left-open interval $(-\infty, a)$ under the inclusion map $(-\infty, a) \hookrightarrow \alpha$ is equal to the left-neighborhood filter $\mathcal{N}_{[<]}(a)$ at $a$.
tendsto_comp_coe_Ioo_atTop theorem
(h : a < b) : Tendsto (fun x : Ioo a b => f x) atTop l ↔ Tendsto f (𝓝[<] b) l
Full source 
@[simp]
theorem tendsto_comp_coe_Ioo_atTop (h : a < b) :
    TendstoTendsto (fun x : Ioo a b => f x) atTop l ↔ Tendsto f (𝓝[<] b) l := by
  rw [← map_coe_Ioo_atTop h, tendsto_map'_iff]; rfl
Limit of Composition on $(a, b)$ at Infinity vs Left Limit at $b$
Informal description
Let $\alpha$ be a preordered topological space with the order topology, and let $a, b \in \alpha$ with $a < b$. For any function $f : \alpha \to \beta$ and any filter $l$ on $\beta$, the composition $f \circ \iota$ tends to $l$ as $x$ tends to $+\infty$ in the open interval $(a, b)$ (where $\iota : (a, b) \hookrightarrow \alpha$ is the inclusion map) if and only if $f$ tends to $l$ as $x$ approaches $b$ from the left in $\alpha$.
tendsto_comp_coe_Ioo_atBot theorem
(h : a < b) : Tendsto (fun x : Ioo a b => f x) atBot l ↔ Tendsto f (𝓝[>] a) l
Full source 
@[simp]
theorem tendsto_comp_coe_Ioo_atBot (h : a < b) :
    TendstoTendsto (fun x : Ioo a b => f x) atBot l ↔ Tendsto f (𝓝[>] a) l := by
  rw [← map_coe_Ioo_atBot h, tendsto_map'_iff]; rfl
Limit of Composition on $(a, b)$ at Negative Infinity vs Right Limit at $a$
Informal description
Let $\alpha$ be a preordered topological space with the order topology, and let $a, b \in \alpha$ with $a < b$. For any function $f : \alpha \to \beta$ and any filter $l$ on $\beta$, the composition $f \circ \iota$ tends to $l$ as $x$ tends to $-\infty$ in the open interval $(a, b)$ (where $\iota : (a, b) \hookrightarrow \alpha$ is the inclusion map) if and only if $f$ tends to $l$ as $x$ approaches $a$ from the right in $\alpha$.
tendsto_comp_coe_Ioi_atBot theorem
: Tendsto (fun x : Ioi a => f x) atBot l ↔ Tendsto f (𝓝[>] a) l
Full source 
@[simp]
theorem tendsto_comp_coe_Ioi_atBot :
    TendstoTendsto (fun x : Ioi a => f x) atBot l ↔ Tendsto f (𝓝[>] a) l := by
  rw [← map_coe_Ioi_atBot, tendsto_map'_iff]; rfl
Limit of Composition on $(a, \infty)$ at Negative Infinity vs Right Limit at $a$
Informal description
Let $\alpha$ be a preordered topological space with the order topology, and let $a \in \alpha$. For any function $f \colon \alpha \to \beta$ and any filter $l$ on $\beta$, the composition $f \circ \iota$ tends to $l$ as $x$ tends to $-\infty$ in the interval $(a, \infty)$ (where $\iota \colon (a, \infty) \hookrightarrow \alpha$ is the inclusion map) if and only if $f$ tends to $l$ as $x$ approaches $a$ from the right in $\alpha$.
tendsto_comp_coe_Iio_atTop theorem
: Tendsto (fun x : Iio a => f x) atTop l ↔ Tendsto f (𝓝[<] a) l
Full source 
@[simp]
theorem tendsto_comp_coe_Iio_atTop :
    TendstoTendsto (fun x : Iio a => f x) atTop l ↔ Tendsto f (𝓝[<] a) l := by
  rw [← map_coe_Iio_atTop, tendsto_map'_iff]; rfl
Limit of Composition on $(-\infty, a)$ at Infinity vs Left Limit at $a$
Informal description
Let $\alpha$ be a preordered topological space with the order topology, and let $a \in \alpha$. For any function $f \colon \alpha \to \beta$ and any filter $l$ on $\beta$, the composition $f \circ \iota$ tends to $l$ as $x$ tends to $+\infty$ in the interval $(-\infty, a)$ (where $\iota \colon (-\infty, a) \hookrightarrow \alpha$ is the inclusion map) if and only if $f$ tends to $l$ as $x$ approaches $a$ from the left in $\alpha$.
tendsto_Ioo_atTop theorem
{f : β → Ioo a b} : Tendsto f l atTop ↔ Tendsto (fun x => (f x : α)) l (𝓝[<] b)
Full source 
@[simp]
theorem tendsto_Ioo_atTop {f : β → Ioo a b} :
    TendstoTendsto f l atTop ↔ Tendsto (fun x => (f x : α)) l (𝓝[<] b) := by
  rw [← comap_coe_Ioo_nhdsLT, tendsto_comap_iff]; rfl
Equivalence of Tendency to Infinity in Open Interval and Left-Neighborhood Filter at Endpoint
Informal description
Let $\alpha$ be a topological space with an order topology, and let $(a, b)$ be an open interval in $\alpha$. For a function $f \colon \beta \to (a, b)$, the following are equivalent: 1. The function $f$ tends to the filter at infinity on $(a, b)$ as its input tends to $l$. 2. The composition of $f$ with the inclusion map $(a, b) \hookrightarrow \alpha$ tends to the left-neighborhood filter of $b$ as its input tends to $l$. In other words, $\lim_{x \to l} f(x) = \infty$ in $(a, b)$ if and only if $\lim_{x \to l} f(x) = b^-$ in $\alpha$.
tendsto_Ioo_atBot theorem
{f : β → Ioo a b} : Tendsto f l atBot ↔ Tendsto (fun x => (f x : α)) l (𝓝[>] a)
Full source 
@[simp]
theorem tendsto_Ioo_atBot {f : β → Ioo a b} :
    TendstoTendsto f l atBot ↔ Tendsto (fun x => (f x : α)) l (𝓝[>] a) := by
  rw [← comap_coe_Ioo_nhdsGT, tendsto_comap_iff]; rfl
Equivalence of Tendency to Negative Infinity in Open Interval and Right-Neighborhood Filter at Endpoint
Informal description
Let $\alpha$ be a topological space with an order topology, and let $(a,b)$ be an open interval in $\alpha$. For a function $f \colon \beta \to (a,b)$, the following are equivalent: 1. The function $f$ tends to the filter at negative infinity on $(a,b)$ as its input tends to $l$. 2. The composition of $f$ with the inclusion map $(a,b) \hookrightarrow \alpha$ tends to the right-neighborhood filter of $a$ as its input tends to $l$. In other words, $\lim_{x \to l} f(x) = -\infty$ in $(a,b)$ if and only if $\lim_{x \to l} f(x) = a^+$ in $\alpha$.
tendsto_Ioi_atBot theorem
{f : β → Ioi a} : Tendsto f l atBot ↔ Tendsto (fun x => (f x : α)) l (𝓝[>] a)
Full source 
@[simp]
theorem tendsto_Ioi_atBot {f : β → Ioi a} :
    TendstoTendsto f l atBot ↔ Tendsto (fun x => (f x : α)) l (𝓝[>] a) := by
  rw [← comap_coe_Ioi_nhdsGT, tendsto_comap_iff]; rfl
Equivalence of Tendency to Negative Infinity in Right-Infinite Interval and Right-Neighborhood Filter at Endpoint
Informal description
Let $\alpha$ be a topological space with an order topology, and let $(a, \infty)$ be the left-open right-infinite interval in $\alpha$. For a function $f \colon \beta \to (a, \infty)$, the following are equivalent: 1. The function $f$ tends to the filter at negative infinity on $(a, \infty)$ as its input tends to $l$. 2. The composition of $f$ with the inclusion map $(a, \infty) \hookrightarrow \alpha$ tends to the right-neighborhood filter of $a$ as its input tends to $l$. In other words, $\lim_{x \to l} f(x) = -\infty$ in $(a, \infty)$ if and only if $\lim_{x \to l} f(x) = a^+$ in $\alpha$.
tendsto_Iio_atTop theorem
{f : β → Iio a} : Tendsto f l atTop ↔ Tendsto (fun x => (f x : α)) l (𝓝[<] a)
Full source 
@[simp]
theorem tendsto_Iio_atTop {f : β → Iio a} :
    TendstoTendsto f l atTop ↔ Tendsto (fun x => (f x : α)) l (𝓝[<] a) := by
  rw [← comap_coe_Iio_nhdsLT, tendsto_comap_iff]; rfl
Equivalence of Tendency to Positive Infinity in Left-Infinite Interval and Left-Neighborhood Filter at Endpoint
Informal description
Let $\alpha$ be a topological space with an order topology, and let $(-\infty, a)$ be the left-infinite right-open interval in $\alpha$. For a function $f \colon \beta \to (-\infty, a)$, the following are equivalent: 1. The function $f$ tends to the filter at positive infinity on $(-\infty, a)$ as its input tends to $l$. 2. The composition of $f$ with the inclusion map $(-\infty, a) \hookrightarrow \alpha$ tends to the left-neighborhood filter of $a$ as its input tends to $l$. In other words, $\lim_{x \to l} f(x) = +\infty$ in $(-\infty, a)$ if and only if $\lim_{x \to l} f(x) = a^-$ in $\alpha$.
instNeBotNhdsWithinComplSetSingletonOfNontrivial instance
(x : α) [Nontrivial α] : NeBot (𝓝[≠] x)
Full source 
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⟩⟩
Nonempty Neighborhood Filter in Complement of Singleton for Nontrivial Order Topology
Informal description
For any nontrivial topological space $\alpha$ with an order topology and any point $x \in \alpha$, the neighborhood filter of $x$ restricted to the complement of $\{x\}$ is nonempty.
Dense.exists_countable_dense_subset_no_bot_top theorem
[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
Full source 
/-- 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]
Existence of Countable Dense Subset Avoiding Extremal Elements in Densely Ordered Spaces
Informal description
Let $\alpha$ be a nontrivial densely ordered topological space, and let $s$ be a dense subset of $\alpha$ that is separable. Then there exists a countable subset $t \subseteq s$ such that: 1. $t$ is dense in $\alpha$, 2. $t$ does not contain any bottom elements of $\alpha$ (i.e., if $x$ is a bottom element, then $x \notin t$), 3. $t$ does not contain any top elements of $\alpha$ (i.e., if $x$ is a top element, then $x \notin t$).
exists_countable_dense_no_bot_top theorem
[SeparableSpace α] [Nontrivial α] : ∃ s : Set α, s.Countable ∧ Dense s ∧ (∀ x, IsBot x → x ∉ s) ∧ ∀ x, IsTop x → x ∉ s
Full source 
/-- 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
Existence of Countable Dense Subset Avoiding Extremal Elements in Densely Ordered Spaces
Informal description
Let $\alpha$ be a nontrivial separable densely ordered topological space. Then there exists a countable dense subset $s \subseteq \alpha$ such that: 1. $s$ does not contain any bottom elements of $\alpha$ (i.e., if $x$ is a bottom element, then $x \notin s$), 2. $s$ does not contain any top elements of $\alpha$ (i.e., if $x$ is a top element, then $x \notin s$).
isClosed_Ico_iff theorem
{a b : α} : IsClosed (Set.Ico a b) ↔ b ≤ a
Full source 
/-- `Set.Ico a b` is only closed if it is empty. -/
@[simp]
theorem isClosed_Ico_iff {a b : α} : IsClosedIsClosed (Set.Ico a b) ↔ b ≤ a := by
  refine ⟨fun h => le_of_not_lt fun hab => ?_, by simp_all⟩
  have := h.closure_eq
  rw [closure_Ico hab.ne, Icc_eq_Ico_same_iff] at this
  exact this hab.le
Closedness of Left-Closed Right-Open Interval: $\text{IsClosed}([a, b)) \leftrightarrow b \leq a$
Informal description
For any elements $a$ and $b$ in a densely ordered topological space $\alpha$, the left-closed right-open interval $[a, b)$ is closed if and only if $b \leq a$.
isClosed_Ioc_iff theorem
{a b : α} : IsClosed (Set.Ioc a b) ↔ b ≤ a
Full source 
/-- `Set.Ioc a b` is only closed if it is empty. -/
@[simp]
theorem isClosed_Ioc_iff {a b : α} : IsClosedIsClosed (Set.Ioc a b) ↔ b ≤ a := by
  refine ⟨fun h => le_of_not_lt fun hab => ?_, by simp_all⟩
  have := h.closure_eq
  rw [closure_Ioc hab.ne, Icc_eq_Ioc_same_iff] at this
  exact this hab.le
Closedness Criterion for Left-Open Right-Closed Interval: $\text{IsClosed}((a, b]) \leftrightarrow b \leq a$
Informal description
For any elements $a$ and $b$ in a densely ordered topological space $\alpha$, the left-open right-closed interval $(a, b]$ is closed if and only if $b \leq a$.
isClosed_Ioo_iff theorem
{a b : α} : IsClosed (Set.Ioo a b) ↔ b ≤ a
Full source 
/-- `Set.Ioo a b` is only closed if it is empty. -/
@[simp]
theorem isClosed_Ioo_iff {a b : α} : IsClosedIsClosed (Set.Ioo a b) ↔ b ≤ a := by
  refine ⟨fun h => le_of_not_lt fun hab => ?_, by simp_all⟩
  have := h.closure_eq
  rw [closure_Ioo hab.ne, Icc_eq_Ioo_same_iff] at this
  exact this hab.le
Closedness of Open Interval in Densely Ordered Space: $\text{IsClosed}((a, b)) \leftrightarrow b \leq a$
Informal description
For any elements $a$ and $b$ in a densely ordered topological space $\alpha$, the open interval $(a, b)$ is closed if and only if $b \leq a$.