Mathlib.Topology.Order.LeftRightNhds

TFAE_mem_nhdsGT theorem

 {a b : α} (hab : a < b) (s : Set α) :
  TFAE [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s]

Full source

/-- The following statements are equivalent:

0. `s` is a neighborhood of `a` within `(a, +∞)`;
1. `s` is a neighborhood of `a` within `(a, b]`;
2. `s` is a neighborhood of `a` within `(a, b)`;
3. `s` includes `(a, u)` for some `u ∈ (a, b]`;
4. `s` includes `(a, u)` for some `u > a`.
-/
theorem TFAE_mem_nhdsGT {a b : α} (hab : a < b) (s : Set α) :
    TFAE [s ∈ 𝓝[>] a,
      s ∈ 𝓝[Ioc a b] a,
      s ∈ 𝓝[Ioo a b] a,
      ∃ u ∈ Ioc a b, Ioo a u ⊆ s,
      ∃ u ∈ Ioi a, Ioo a u ⊆ s] := by
  tfae_have 1 ↔ 2 := by
    rw [nhdsWithin_Ioc_eq_nhdsGT hab]
  tfae_have 1 ↔ 3 := by
    rw [nhdsWithin_Ioo_eq_nhdsGT hab]
  tfae_have 4 → 5 := fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩
  tfae_have 5 → 1
  | ⟨u, hau, hu⟩ => mem_of_superset (Ioo_mem_nhdsGT hau) hu
  tfae_have 1 → 4
  | h => by
    rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 h with ⟨v, va, hv⟩
    rcases exists_Ico_subset_of_mem_nhds' va hab with ⟨u, au, hu⟩
    exact ⟨u, au, fun x hx => hv ⟨hu ⟨le_of_lt hx.1, hx.2⟩, hx.1⟩⟩
  tfae_finish

Equivalence of Right Neighborhood Conditions in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a < b$ be elements of $\alpha$. For any set $s \subseteq \alpha$, the following statements are equivalent: 1. $s$ is a neighborhood of $a$ within the right-infinite interval $(a, +\infty)$; 2. $s$ is a neighborhood of $a$ within the right-closed interval $(a, b]$; 3. $s$ is a neighborhood of $a$ within the open interval $(a, b)$; 4. There exists $u \in (a, b]$ such that the open interval $(a, u)$ is contained in $s$; 5. There exists $u > a$ such that the open interval $(a, u)$ is contained in $s$.

mem_nhdsGT_iff_exists_mem_Ioc_Ioo_subset theorem

{a u' : α} {s : Set α} (hu' : a < u') : s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioc a u', Ioo a u ⊆ s

Full source

theorem mem_nhdsGT_iff_exists_mem_Ioc_Ioo_subset {a u' : α} {s : Set α} (hu' : a < u') :
    s ∈ 𝓝[>] as ∈ 𝓝[>] a ↔ ∃ u ∈ Ioc a u', Ioo a u ⊆ s :=
  (TFAE_mem_nhdsGT hu' s).out 0 3

Characterization of Right Neighborhoods via Right-Closed Intervals

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a < u'$ be elements of $\alpha$. For any set $s \subseteq \alpha$, the following are equivalent: - $s$ is a neighborhood of $a$ within the right-infinite interval $(a, +\infty)$; - There exists $u \in (a, u']$ such that the open interval $(a, u)$ is contained in $s$.

mem_nhdsGT_iff_exists_Ioo_subset' theorem

{a u' : α} {s : Set α} (hu' : a < u') : s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioo a u ⊆ s

Full source

/-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u)`
with `a < u < u'`, provided `a` is not a top element. -/
theorem mem_nhdsGT_iff_exists_Ioo_subset' {a u' : α} {s : Set α} (hu' : a < u') :
    s ∈ 𝓝[>] as ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioo a u ⊆ s :=
  (TFAE_mem_nhdsGT hu' s).out 0 4

Characterization of Right Neighborhoods via Open Intervals

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a < u'$ be elements of $\alpha$. For any set $s \subseteq \alpha$, the following are equivalent: - $s$ is a neighborhood of $a$ within the right-infinite interval $(a, +\infty)$; - There exists $u > a$ such that the open interval $(a, u)$ is contained in $s$.

nhdsGT_basis_of_exists_gt theorem

{a : α} (h : ∃ b, a < b) : (𝓝[>] a).HasBasis (a < ·) (Ioo a)

Full source

theorem nhdsGT_basis_of_exists_gt {a : α} (h : ∃ b, a < b) : (𝓝[>] a).HasBasis (a < ·) (Ioo a) :=
  let ⟨_, h⟩ := h
  ⟨fun _ => mem_nhdsGT_iff_exists_Ioo_subset' h⟩

Basis Characterization of Right Neighborhood Filter via Open Intervals

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a \in \alpha$ be an element for which there exists some $b > a$. Then the right neighborhood filter $\mathcal{N}_{>}(a)$ has a basis consisting of open intervals $(a, u)$ for all $u > a$.

nhdsGT_basis theorem

[NoMaxOrder α] (a : α) : (𝓝[>] a).HasBasis (a < ·) (Ioo a)

Full source

lemma nhdsGT_basis [NoMaxOrder α] (a : α) : (𝓝[>] a).HasBasis (a < ·) (Ioo a) :=
  nhdsGT_basis_of_exists_gt <| exists_gt a

Basis of Right Neighborhood Filter via Open Intervals in Order Topology without Maximal Element

Informal description

Let $\alpha$ be a topological space with an order topology and no maximal element. For any element $a \in \alpha$, the right neighborhood filter $\mathcal{N}_{>}(a)$ has a basis consisting of open intervals $(a, u)$ for all $u > a$.

nhdsGT_eq_bot_iff theorem

{a : α} : 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b

Full source

theorem nhdsGT_eq_bot_iff {a : α} : 𝓝[>] a𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b := by
  by_cases ha : IsTop a
  · simp [ha, ha.isMax.Ioi_eq]
  · simp only [ha, false_or]
    rw [isTop_iff_isMax, not_isMax_iff] at ha
    simp only [(nhdsGT_basis_of_exists_gt ha).eq_bot_iff, covBy_iff_Ioo_eq]

Triviality of Right Neighborhood Filter in Order Topology: $\mathcal{N}_{>}(a) = \bot$ iff $a$ is Top or Covered

Informal description

For any element $a$ in a topological space $\alpha$ with an order topology, the right neighborhood filter $\mathcal{N}_{>}(a)$ is trivial (equal to the bottom filter) if and only if either $a$ is a top element in $\alpha$ or there exists an element $b$ that covers $a$ (i.e., $a$ is immediately below $b$ with no elements strictly between them).

mem_nhdsGT_iff_exists_Ioo_subset theorem

[NoMaxOrder α] {a : α} {s : Set α} : s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioo a u ⊆ s

Full source

/-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u)`
with `a < u`. -/
theorem mem_nhdsGT_iff_exists_Ioo_subset [NoMaxOrder α] {a : α} {s : Set α} :
    s ∈ 𝓝[>] as ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioo a u ⊆ s :=
  let ⟨_u', hu'⟩ := exists_gt a
  mem_nhdsGT_iff_exists_Ioo_subset' hu'

Characterization of Right Neighborhoods via Open Intervals in Order Topology without Maximal Element

Informal description

Let $\alpha$ be a topological space with an order topology and no maximal element. For any point $a \in \alpha$ and any subset $s \subseteq \alpha$, the following are equivalent: - $s$ is a neighborhood of $a$ within the right-infinite interval $(a, +\infty)$; - There exists $u > a$ such that the open interval $(a, u)$ is contained in $s$.

countable_setOf_isolated_right theorem

[SecondCountableTopology α] : {x : α | 𝓝[>] x = ⊥}.Countable

Full source

/-- The set of points which are isolated on the right is countable when the space is
second-countable. -/
theorem countable_setOf_isolated_right [SecondCountableTopology α] :
    { x : α | 𝓝[>] x = ⊥ }.Countable := by
  simp only [nhdsGT_eq_bot_iff, setOf_or]
  exact (subsingleton_isTop α).countable.union countable_setOf_covBy_right

Countability of Right-Isolated Points in Second-Countable Order Topology

Informal description

In a second-countable topological space $\alpha$ with an order topology, the set of points $x \in \alpha$ that are isolated on the right (i.e., points where the right neighborhood filter $\mathcal{N}_{>x}$ is trivial) is countable.

countable_setOf_isolated_left theorem

[SecondCountableTopology α] : {x : α | 𝓝[<] x = ⊥}.Countable

Full source

/-- The set of points which are isolated on the left is countable when the space is
second-countable. -/
theorem countable_setOf_isolated_left [SecondCountableTopology α] :
    { x : α | 𝓝[<] x = ⊥ }.Countable :=
  countable_setOf_isolated_right (α := αᵒᵈ)

Countability of Left-Isolated Points in Second-Countable Order Topology

Informal description

In a second-countable topological space $\alpha$ with an order topology, the set of points $x \in \alpha$ that are isolated on the left (i.e., points where the left neighborhood filter $\mathcal{N}_{

mem_nhdsGT_iff_exists_Ioc_subset theorem

[NoMaxOrder α] [DenselyOrdered α] {a : α} {s : Set α} : s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s

Full source

/-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u]`
with `a < u`. -/
theorem mem_nhdsGT_iff_exists_Ioc_subset [NoMaxOrder α] [DenselyOrdered α] {a : α} {s : Set α} :
    s ∈ 𝓝[>] as ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s := by
  rw [mem_nhdsGT_iff_exists_Ioo_subset]
  constructor
  · rintro ⟨u, au, as⟩
    rcases exists_between au with ⟨v, hv⟩
    exact ⟨v, hv.1, fun x hx => as ⟨hx.1, lt_of_le_of_lt hx.2 hv.2⟩⟩
  · rintro ⟨u, au, as⟩
    exact ⟨u, au, Subset.trans Ioo_subset_Ioc_self as⟩

Characterization of Right Neighborhoods via Half-Open Intervals in Densely Ordered Topology

Informal description

Let $\alpha$ be a topological space with an order topology that is densely ordered and has no maximal element. For any point $a \in \alpha$ and any subset $s \subseteq \alpha$, the following are equivalent: - $s$ is a neighborhood of $a$ within the right-infinite interval $(a, +\infty)$; - There exists $u > a$ such that the left-open right-closed interval $(a, u]$ is contained in $s$.

TFAE_mem_nhdsLT theorem

 {a b : α} (h : a < b) (s : Set α) :
  TFAE
    [s ∈ 𝓝[<] b,
      -- 0 : `s` is a neighborhood of `b` within `(-∞, b)`s ∈ 𝓝[Ico a b] b,
      -- 1 : `s` is a neighborhood of `b` within `[a, b)`s ∈ 𝓝[Ioo a b] b,
      -- 2 : `s` is a neighborhood of `b` within `(a, b)`∃ l ∈ Ico a b, Ioo l b ⊆ s,
      -- 3 : `s` includes `(l, b)` for some `l ∈ [a, b)`∃ l ∈ Iio b, Ioo l b ⊆ s]

Full source

/-- The following statements are equivalent:

0. `s` is a neighborhood of `b` within `(-∞, b)`
1. `s` is a neighborhood of `b` within `[a, b)`
2. `s` is a neighborhood of `b` within `(a, b)`
3. `s` includes `(l, b)` for some `l ∈ [a, b)`
4. `s` includes `(l, b)` for some `l < b` -/
theorem TFAE_mem_nhdsLT {a b : α} (h : a < b) (s : Set α) :
    TFAE [s ∈ 𝓝[<] b,-- 0 : `s` is a neighborhood of `b` within `(-∞, b)`
        s ∈ 𝓝[Ico a b] b,-- 1 : `s` is a neighborhood of `b` within `[a, b)`
        s ∈ 𝓝[Ioo a b] b,-- 2 : `s` is a neighborhood of `b` within `(a, b)`
        ∃ l ∈ Ico a b, Ioo l b ⊆ s,-- 3 : `s` includes `(l, b)` for some `l ∈ [a, b)`
        ∃ l ∈ Iio b, Ioo l b ⊆ s] := by-- 4 : `s` includes `(l, b)` for some `l < b`
  simpa using TFAE_mem_nhdsGT h.dual (ofDualofDual ⁻¹' s)

Equivalence of Left Neighborhood Conditions in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a < b$ be elements of $\alpha$. For any set $s \subseteq \alpha$, the following statements are equivalent: 1. $s$ is a neighborhood of $b$ within the left-infinite interval $(-\infty, b)$; 2. $s$ is a neighborhood of $b$ within the left-closed interval $[a, b)$; 3. $s$ is a neighborhood of $b$ within the open interval $(a, b)$; 4. There exists $l \in [a, b)$ such that the open interval $(l, b)$ is contained in $s$; 5. There exists $l < b$ such that the open interval $(l, b)$ is contained in $s$.

mem_nhdsLT_iff_exists_mem_Ico_Ioo_subset theorem

{a l' : α} {s : Set α} (hl' : l' < a) : s ∈ 𝓝[<] a ↔ ∃ l ∈ Ico l' a, Ioo l a ⊆ s

Full source

theorem mem_nhdsLT_iff_exists_mem_Ico_Ioo_subset {a l' : α} {s : Set α} (hl' : l' < a) :
    s ∈ 𝓝[<] as ∈ 𝓝[<] a ↔ ∃ l ∈ Ico l' a, Ioo l a ⊆ s :=
  (TFAE_mem_nhdsLT hl' s).out 0 3

Characterization of Left Neighborhoods via Half-Open Intervals in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a, l' \in \alpha$ with $l' < a$. For any subset $s \subseteq \alpha$, the following are equivalent: 1. $s$ is a neighborhood of $a$ within the left-infinite interval $(-\infty, a)$; 2. There exists $l \in [l', a)$ such that the open interval $(l, a)$ is contained in $s$.

mem_nhdsLT_iff_exists_Ioo_subset' theorem

{a l' : α} {s : Set α} (hl' : l' < a) : s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ioo l a ⊆ s

Full source

/-- A set is a neighborhood of `a` within `(-∞, a)` if and only if it contains an interval `(l, a)`
with `l < a`, provided `a` is not a bottom element. -/
theorem mem_nhdsLT_iff_exists_Ioo_subset' {a l' : α} {s : Set α} (hl' : l' < a) :
    s ∈ 𝓝[<] as ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ioo l a ⊆ s :=
  (TFAE_mem_nhdsLT hl' s).out 0 4

Characterization of Left Neighborhoods via Open Intervals in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a$ be an element of $\alpha$ that is not a minimal element. For any set $s \subseteq \alpha$, the following are equivalent: 1. $s$ is a neighborhood of $a$ within the left-infinite interval $(-\infty, a)$; 2. There exists $l < a$ such that the open interval $(l, a)$ is contained in $s$.

mem_nhdsLT_iff_exists_Ioo_subset theorem

[NoMinOrder α] {a : α} {s : Set α} : s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ioo l a ⊆ s

Full source

/-- A set is a neighborhood of `a` within `(-∞, a)` if and only if it contains an interval `(l, a)`
with `l < a`. -/
theorem mem_nhdsLT_iff_exists_Ioo_subset [NoMinOrder α] {a : α} {s : Set α} :
    s ∈ 𝓝[<] as ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ioo l a ⊆ s :=
  let ⟨_, h⟩ := exists_lt a
  mem_nhdsLT_iff_exists_Ioo_subset' h

Characterization of Left Neighborhoods via Open Intervals in Order Topology Without Minimal Elements

Informal description

Let $\alpha$ be a topological space with an order topology and no minimal elements. For any point $a \in \alpha$ and any subset $s \subseteq \alpha$, the following are equivalent: 1. $s$ is a neighborhood of $a$ within the left-infinite interval $(-\infty, a)$; 2. There exists $l < a$ such that the open interval $(l, a)$ is contained in $s$.

mem_nhdsLT_iff_exists_Ico_subset theorem

[NoMinOrder α] [DenselyOrdered α] {a : α} {s : Set α} : s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ico l a ⊆ s

Full source

/-- A set is a neighborhood of `a` within `(-∞, a)` if and only if it contains an interval `[l, a)`
with `l < a`. -/
theorem mem_nhdsLT_iff_exists_Ico_subset [NoMinOrder α] [DenselyOrdered α] {a : α} {s : Set α} :
    s ∈ 𝓝[<] as ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ico l a ⊆ s := by
  have : ofDualofDual ⁻¹' sofDual ⁻¹' s ∈ 𝓝[>] toDual aofDual ⁻¹' s ∈ 𝓝[>] toDual a ↔ _ := mem_nhdsGT_iff_exists_Ioc_subset
  simpa using this

Characterization of Left Neighborhoods via Left-Closed Right-Open Intervals in Densely Ordered Topology

Informal description

Let $\alpha$ be a topological space with an order topology that is densely ordered and has no minimal element. For any point $a \in \alpha$ and any subset $s \subseteq \alpha$, the following are equivalent: - $s$ is a neighborhood of $a$ within the left-infinite interval $(-\infty, a)$; - There exists $l < a$ such that the left-closed right-open interval $[l, a)$ is contained in $s$.

nhdsLT_basis_of_exists_lt theorem

{a : α} (h : ∃ b, b < a) : (𝓝[<] a).HasBasis (· < a) (Ioo · a)

Full source

theorem nhdsLT_basis_of_exists_lt {a : α} (h : ∃ b, b < a) : (𝓝[<] a).HasBasis (· < a) (Ioo · a) :=
  let ⟨_, h⟩ := h
  ⟨fun _ => mem_nhdsLT_iff_exists_Ioo_subset' h⟩

Basis Characterization of Left-Neighborhood Filter via Open Intervals in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a \in \alpha$ be an element for which there exists some $b < a$. Then the left-neighborhood filter $\mathcal{N}_{<}(a)$ has a basis consisting of the open intervals $(l, a)$ for all $l < a$.

nhdsLT_basis theorem

[NoMinOrder α] (a : α) : (𝓝[<] a).HasBasis (· < a) (Ioo · a)

Full source

theorem nhdsLT_basis [NoMinOrder α] (a : α) : (𝓝[<] a).HasBasis (· < a) (Ioo · a) :=
  nhdsLT_basis_of_exists_lt <| exists_lt a

Basis of Left-Neighborhood Filter in Order Topology Without Minimal Element

Informal description

Let $\alpha$ be a topological space with an order topology and no minimal element. For any element $a \in \alpha$, the left-neighborhood filter $\mathcal{N}_{<}(a)$ has a basis consisting of the open intervals $(l, a)$ for all $l < a$.

nhdsLT_eq_bot_iff theorem

{a : α} : 𝓝[<] a = ⊥ ↔ IsBot a ∨ ∃ b, b ⋖ a

Full source

theorem nhdsLT_eq_bot_iff {a : α} : 𝓝[<] a𝓝[<] a = ⊥ ↔ IsBot a ∨ ∃ b, b ⋖ a := by
  convert (config := { preTransparency := .default }) nhdsGT_eq_bot_iff (a := OrderDual.toDual a)
    using 4
  exact ofDual_covBy_ofDual_iff

Triviality of Left Neighborhood Filter in Order Topology: $\mathcal{N}_{<}(a) = \bot$ iff $a$ is Bottom or Covers

Informal description

For any element $a$ in a topological space $\alpha$ with an order topology, the left neighborhood filter $\mathcal{N}_{<}(a)$ is trivial (equal to the bottom filter) if and only if either $a$ is a bottom element in $\alpha$ or there exists an element $b$ that is covered by $a$ (i.e., $b$ is immediately below $a$ with no elements strictly between them).

TFAE_mem_nhdsGE theorem

 {a b : α} (hab : a < b) (s : Set α) :
  TFAE [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u ∈ Ioc a b, Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s]

Full source

/-- The following statements are equivalent:

0. `s` is a neighborhood of `a` within `[a, +∞)`;
1. `s` is a neighborhood of `a` within `[a, b]`;
2. `s` is a neighborhood of `a` within `[a, b)`;
3. `s` includes `[a, u)` for some `u ∈ (a, b]`;
4. `s` includes `[a, u)` for some `u > a`.
-/
theorem TFAE_mem_nhdsGE {a b : α} (hab : a < b) (s : Set α) :
    TFAE [s ∈ 𝓝[≥] a,
      s ∈ 𝓝[Icc a b] a,
      s ∈ 𝓝[Ico a b] a,
      ∃ u ∈ Ioc a b, Ico a u ⊆ s,
      ∃ u ∈ Ioi a , Ico a u ⊆ s] := by
  tfae_have 1 ↔ 2 := by
    rw [nhdsWithin_Icc_eq_nhdsGE hab]
  tfae_have 1 ↔ 3 := by
    rw [nhdsWithin_Ico_eq_nhdsGE hab]
  tfae_have 1 ↔ 5 := (nhdsGE_basis_of_exists_gt ⟨b, hab⟩).mem_iff
  tfae_have 4 → 5 := fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩
  tfae_have 5 → 4
  | ⟨u, hua, hus⟩ => ⟨min u b, ⟨lt_min hua hab, min_le_right _ _⟩,
      (Ico_subset_Ico_right <| min_le_left _ _).trans hus⟩
  tfae_finish

Equivalence of Right-Neighborhood Conditions in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a, b \in \alpha$ with $a < b$. For any set $s \subseteq \alpha$, the following statements are equivalent: 1. $s$ is a neighborhood of $a$ within the right-closed interval $[a, +\infty)$; 2. $s$ is a neighborhood of $a$ within the closed interval $[a, b]$; 3. $s$ is a neighborhood of $a$ within the right-open interval $[a, b)$; 4. There exists $u \in (a, b]$ such that the interval $[a, u) \subseteq s$; 5. There exists $u > a$ such that the interval $[a, u) \subseteq s$.

mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset theorem

{a u' : α} {s : Set α} (hu' : a < u') : s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioc a u', Ico a u ⊆ s

Full source

theorem mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset {a u' : α} {s : Set α} (hu' : a < u') :
    s ∈ 𝓝[≥] as ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioc a u', Ico a u ⊆ s :=
  (TFAE_mem_nhdsGE hu' s).out 0 3 (by norm_num) (by norm_num)

Characterization of Right-Neighborhoods via Right-Closed Intervals

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a, u' \in \alpha$ with $a < u'$. For any set $s \subseteq \alpha$, the following are equivalent: 1. $s$ is a neighborhood of $a$ within the right-closed interval $[a, +\infty)$; 2. There exists $u \in (a, u']$ such that the left-closed right-open interval $[a, u)$ is contained in $s$.

mem_nhdsGE_iff_exists_Ico_subset' theorem

{a u' : α} {s : Set α} (hu' : a < u') : s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s

Full source

/-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u)`
with `a < u < u'`, provided `a` is not a top element. -/
theorem mem_nhdsGE_iff_exists_Ico_subset' {a u' : α} {s : Set α} (hu' : a < u') :
    s ∈ 𝓝[≥] as ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s :=
  (TFAE_mem_nhdsGE hu' s).out 0 4 (by norm_num) (by norm_num)

Characterization of Right-Neighborhoods via Right-Open Intervals

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a, u' \in \alpha$ with $a < u'$. For any set $s \subseteq \alpha$, the following are equivalent: 1. $s$ is a neighborhood of $a$ within the right-closed interval $[a, +\infty)$; 2. There exists $u > a$ such that the left-closed right-open interval $[a, u)$ is contained in $s$.

mem_nhdsGE_iff_exists_Ico_subset theorem

[NoMaxOrder α] {a : α} {s : Set α} : s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s

Full source

/-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u)`
with `a < u`. -/
theorem mem_nhdsGE_iff_exists_Ico_subset [NoMaxOrder α] {a : α} {s : Set α} :
    s ∈ 𝓝[≥] as ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s :=
  let ⟨_, hu'⟩ := exists_gt a
  mem_nhdsGE_iff_exists_Ico_subset' hu'

Characterization of Right-Neighborhoods via Right-Open Intervals in Order Topology Without Maximal Element

Informal description

Let $\alpha$ be a topological space with an order topology and no maximal element. For any element $a \in \alpha$ and any set $s \subseteq \alpha$, the following are equivalent: 1. $s$ is a neighborhood of $a$ within the right-closed interval $[a, +\infty)$; 2. There exists $u > a$ such that the left-closed right-open interval $[a, u)$ is contained in $s$.

nhdsGE_basis_Ico theorem

[NoMaxOrder α] (a : α) : (𝓝[≥] a).HasBasis (fun u => a < u) (Ico a)

Full source

theorem nhdsGE_basis_Ico [NoMaxOrder α] (a : α) : (𝓝[≥] a).HasBasis (fun u => a < u) (Ico a) :=
  ⟨fun _ => mem_nhdsGE_iff_exists_Ico_subset⟩

Basis of Right Neighborhood Filter via Left-Closed Right-Open Intervals in Order Topology Without Maximal Element

Informal description

Let $\alpha$ be a topological space with an order topology and no maximal element. For any element $a \in \alpha$, the right neighborhood filter $\mathcal{N}_{\geq a}$ has a basis consisting of left-closed right-open intervals $[a, u)$ where $u > a$.

nhdsGE_basis_Icc theorem

[NoMaxOrder α] [DenselyOrdered α] {a : α} : (𝓝[≥] a).HasBasis (a < ·) (Icc a)

Full source

/-- The filter of right neighborhoods has a basis of closed intervals. -/
theorem nhdsGE_basis_Icc [NoMaxOrder α] [DenselyOrdered α] {a : α} :
    (𝓝[≥] a).HasBasis (a < ·) (Icc a) :=
  (nhdsGE_basis _).to_hasBasis
    (fun _u hu ↦ (exists_between hu).imp fun _v hv ↦ hv.imp_right Icc_subset_Ico_right) fun u hu ↦
    ⟨u, hu, Ico_subset_Icc_self⟩

Closed Intervals Form Basis for Right Neighborhood Filter in Densely Ordered Space Without Maximal Element

Informal description

Let $\alpha$ be a densely ordered type with no maximal element. For any element $a \in \alpha$, the right neighborhood filter $\mathcal{N}_{\geq a}$ has a basis consisting of closed intervals $[a, u]$ where $u > a$.

mem_nhdsGE_iff_exists_Icc_subset theorem

[NoMaxOrder α] [DenselyOrdered α] {a : α} {s : Set α} : s ∈ 𝓝[≥] a ↔ ∃ u, a < u ∧ Icc a u ⊆ s

Full source

/-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u]`
with `a < u`. -/
theorem mem_nhdsGE_iff_exists_Icc_subset [NoMaxOrder α] [DenselyOrdered α] {a : α} {s : Set α} :
    s ∈ 𝓝[≥] as ∈ 𝓝[≥] a ↔ ∃ u, a < u ∧ Icc a u ⊆ s :=
  nhdsGE_basis_Icc.mem_iff

Characterization of Right Neighborhoods via Closed Intervals in Densely Ordered Spaces

Informal description

Let $\alpha$ be a densely ordered type with no maximal element. For any element $a \in \alpha$ and any set $s \subseteq \alpha$, $s$ is a neighborhood of $a$ within $[a, \infty)$ if and only if there exists an element $u > a$ such that the closed interval $[a, u]$ is contained in $s$.

TFAE_mem_nhdsLE theorem

 {a b : α} (h : a < b) (s : Set α) :
  TFAE
    [s ∈ 𝓝[≤] b,
      -- 0 : `s` is a neighborhood of `b` within `(-∞, b]`s ∈ 𝓝[Icc a b] b,
      -- 1 : `s` is a neighborhood of `b` within `[a, b]`s ∈ 𝓝[Ioc a b] b,
      -- 2 : `s` is a neighborhood of `b` within `(a, b]`∃ l ∈ Ico a b, Ioc l b ⊆ s,
      -- 3 : `s` includes `(l, b]` for some `l ∈ [a, b)`∃ l ∈ Iio b, Ioc l b ⊆ s]

Full source

/-- The following statements are equivalent:

0. `s` is a neighborhood of `b` within `(-∞, b]`
1. `s` is a neighborhood of `b` within `[a, b]`
2. `s` is a neighborhood of `b` within `(a, b]`
3. `s` includes `(l, b]` for some `l ∈ [a, b)`
4. `s` includes `(l, b]` for some `l < b` -/
theorem TFAE_mem_nhdsLE {a b : α} (h : a < b) (s : Set α) :
    TFAE [s ∈ 𝓝[≤] b,-- 0 : `s` is a neighborhood of `b` within `(-∞, b]`
      s ∈ 𝓝[Icc a b] b,-- 1 : `s` is a neighborhood of `b` within `[a, b]`
      s ∈ 𝓝[Ioc a b] b,-- 2 : `s` is a neighborhood of `b` within `(a, b]`
      ∃ l ∈ Ico a b, Ioc l b ⊆ s,-- 3 : `s` includes `(l, b]` for some `l ∈ [a, b)`
      ∃ l ∈ Iio b, Ioc l b ⊆ s] := by-- 4 : `s` includes `(l, b]` for some `l < b`
  simpa using TFAE_mem_nhdsGE h.dual (ofDualofDual ⁻¹' s)

Equivalence of Left-Neighborhood Conditions in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a, b \in \alpha$ with $a < b$. For any set $s \subseteq \alpha$, the following statements are equivalent: 1. $s$ is a neighborhood of $b$ within the left-closed interval $(-\infty, b]$; 2. $s$ is a neighborhood of $b$ within the closed interval $[a, b]$; 3. $s$ is a neighborhood of $b$ within the left-open interval $(a, b]$; 4. There exists $l \in [a, b)$ such that the interval $(l, b] \subseteq s$; 5. There exists $l < b$ such that the interval $(l, b] \subseteq s$.

mem_nhdsLE_iff_exists_mem_Ico_Ioc_subset theorem

{a l' : α} {s : Set α} (hl' : l' < a) : s ∈ 𝓝[≤] a ↔ ∃ l ∈ Ico l' a, Ioc l a ⊆ s

Full source

theorem mem_nhdsLE_iff_exists_mem_Ico_Ioc_subset {a l' : α} {s : Set α} (hl' : l' < a) :
    s ∈ 𝓝[≤] as ∈ 𝓝[≤] a ↔ ∃ l ∈ Ico l' a, Ioc l a ⊆ s :=
  (TFAE_mem_nhdsLE hl' s).out 0 3 (by norm_num) (by norm_num)

Characterization of Left-Neighborhoods via Left-Open Right-Closed Intervals in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a, l' \in \alpha$ with $l' < a$. For any set $s \subseteq \alpha$, $s$ is a neighborhood of $a$ within the left-closed interval $(-\infty, a]$ if and only if there exists an element $l \in [l', a)$ such that the left-open right-closed interval $(l, a] \subseteq s$.

mem_nhdsLE_iff_exists_Ioc_subset' theorem

{a l' : α} {s : Set α} (hl' : l' < a) : s ∈ 𝓝[≤] a ↔ ∃ l ∈ Iio a, Ioc l a ⊆ s

Full source

/-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `(l, a]`
with `l < a`, provided `a` is not a bottom element. -/
theorem mem_nhdsLE_iff_exists_Ioc_subset' {a l' : α} {s : Set α} (hl' : l' < a) :
    s ∈ 𝓝[≤] as ∈ 𝓝[≤] a ↔ ∃ l ∈ Iio a, Ioc l a ⊆ s :=
  (TFAE_mem_nhdsLE hl' s).out 0 4 (by norm_num) (by norm_num)

Characterization of Left Neighborhoods via Left-Open Right-Closed Intervals

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a, l' \in \alpha$ with $l' < a$. For any set $s \subseteq \alpha$, $s$ is a neighborhood of $a$ within the left-closed interval $(-\infty, a]$ if and only if there exists $l < a$ such that the left-open right-closed interval $(l, a]$ is contained in $s$.

mem_nhdsLE_iff_exists_Ioc_subset theorem

[NoMinOrder α] {a : α} {s : Set α} : s ∈ 𝓝[≤] a ↔ ∃ l ∈ Iio a, Ioc l a ⊆ s

Full source

/-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `(l, a]`
with `l < a`. -/
theorem mem_nhdsLE_iff_exists_Ioc_subset [NoMinOrder α] {a : α} {s : Set α} :
    s ∈ 𝓝[≤] as ∈ 𝓝[≤] a ↔ ∃ l ∈ Iio a, Ioc l a ⊆ s :=
  let ⟨_, hl'⟩ := exists_lt a
  mem_nhdsLE_iff_exists_Ioc_subset' hl'

Characterization of Left Neighborhoods via Left-Open Right-Closed Intervals in Order Topology without Minimal Element

Informal description

Let $\alpha$ be a topological space with an order topology and no minimal element. For any element $a \in \alpha$ and any set $s \subseteq \alpha$, $s$ is a neighborhood of $a$ within the left-closed interval $(-\infty, a]$ if and only if there exists an element $l < a$ such that the left-open right-closed interval $(l, a]$ is contained in $s$.

mem_nhdsLE_iff_exists_Icc_subset theorem

[NoMinOrder α] [DenselyOrdered α] {a : α} {s : Set α} : s ∈ 𝓝[≤] a ↔ ∃ l, l < a ∧ Icc l a ⊆ s

Full source

/-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `[l, a]`
with `l < a`. -/
theorem mem_nhdsLE_iff_exists_Icc_subset [NoMinOrder α] [DenselyOrdered α] {a : α}
    {s : Set α} : s ∈ 𝓝[≤] as ∈ 𝓝[≤] a ↔ ∃ l, l < a ∧ Icc l a ⊆ s :=
  calc s ∈ 𝓝[≤] a ↔ ofDual ⁻¹' s ∈ 𝓝[≥] (toDual a) := Iff.rfl
  _ ↔ ∃ u : α, toDual a < toDual u ∧ Icc (toDual a) (toDual u) ⊆ ofDual ⁻¹' scalc s ∈ 𝓝[≤] a ↔ ofDual ⁻¹' s ∈ 𝓝[≥] (toDual a) := Iff.rfl
  _ ↔ ∃ u : α, toDual a < toDual u ∧ Icc (toDual a) (toDual u) ⊆ ofDual ⁻¹' s :=
    mem_nhdsGE_iff_exists_Icc_subset
  _ ↔ ∃ l, l < a ∧ Icc l a ⊆ s := by simp

Characterization of Left Neighborhoods via Closed Intervals in Densely Ordered Spaces

Informal description

Let $\alpha$ be a densely ordered type with no minimal element. For any element $a \in \alpha$ and any set $s \subseteq \alpha$, $s$ is a neighborhood of $a$ within $(-\infty, a]$ if and only if there exists an element $l < a$ such that the closed interval $[l, a]$ is contained in $s$.

nhdsLE_basis_Icc theorem

[NoMinOrder α] [DenselyOrdered α] {a : α} : (𝓝[≤] a).HasBasis (· < a) (Icc · a)

Full source

/-- The filter of left neighborhoods has a basis of closed intervals. -/
theorem nhdsLE_basis_Icc [NoMinOrder α] [DenselyOrdered α] {a : α} :
    (𝓝[≤] a).HasBasis (· < a) (Icc · a) :=
  ⟨fun _ ↦ mem_nhdsLE_iff_exists_Icc_subset⟩

Basis of Left Neighborhoods via Closed Intervals in Densely Ordered Spaces

Informal description

Let $\alpha$ be a densely ordered type with no minimal element. For any element $a \in \alpha$, the filter of left neighborhoods $\mathcal{N}_{\leq}(a)$ has a basis consisting of closed intervals $[l, a]$ where $l$ ranges over all elements less than $a$.

nhds_eq_iInf_mabs_div theorem

(a : α) : 𝓝 a = ⨅ r > 1, 𝓟 {b | |a / b|ₘ < r}

Full source

@[to_additive]
theorem nhds_eq_iInf_mabs_div (a : α) : 𝓝 a = ⨅ r > 1, 𝓟 { b | |a / b|ₘ < r } := by
  simp only [nhds_eq_order, mabs_lt, setOf_and, ← inf_principal, iInf_inf_eq]
  refine (congr_arg₂ _ ?_ ?_).trans (inf_comm ..)
  · refine (Equiv.divLeft a).iInf_congr fun x => ?_; simp [Ioi]
  · refine (Equiv.divRight a).iInf_congr fun x => ?_; simp [Iio]

Neighborhood Filter Characterization via Multiplicative Absolute Value

Informal description

Let $\alpha$ be a topological space with a commutative group structure and a linear order, forming an ordered monoid. For any element $a \in \alpha$, the neighborhood filter $\mathcal{N}(a)$ can be expressed as the infimum over all $r > 1$ of the principal filters generated by the sets $\{b \mid |a/b|_m < r\}$, where $| \cdot |_m$ denotes the multiplicative absolute value.

orderTopology_of_nhds_mabs theorem

 {α : Type*} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α]
  (h_nhds : ∀ a : α, 𝓝 a = ⨅ r > 1, 𝓟 {b | |a / b|ₘ < r}) : OrderTopology α

Full source

@[to_additive]
theorem orderTopology_of_nhds_mabs {α : Type*} [TopologicalSpace α] [CommGroup α] [LinearOrder α]
    [IsOrderedMonoid α]
    (h_nhds : ∀ a : α, 𝓝 a = ⨅ r > 1, 𝓟 { b | |a / b|ₘ < r }) : OrderTopology α := by
  refine ⟨TopologicalSpace.ext_nhds fun a => ?_⟩
  rw [h_nhds]
  letI := Preorder.topology α; letI : OrderTopology α := ⟨rfl⟩
  exact (nhds_eq_iInf_mabs_div a).symm

Characterization of Order Topology via Multiplicative Absolute Value Neighborhoods

Informal description

Let $\alpha$ be a topological space equipped with a commutative group structure and a linear order, forming an ordered monoid. If for every element $a \in \alpha$, the neighborhood filter $\mathcal{N}(a)$ can be expressed as the infimum over all $r > 1$ of the principal filters generated by the sets $\{b \mid |a / b|_m < r\}$, where $|\cdot|_m$ denotes the multiplicative absolute value, then the topology on $\alpha$ is the order topology.

LinearOrderedCommGroup.tendsto_nhds theorem

{x : Filter β} {a : α} : Tendsto f x (𝓝 a) ↔ ∀ ε > (1 : α), ∀ᶠ b in x, |f b / a|ₘ < ε

Full source

@[to_additive]
theorem LinearOrderedCommGroup.tendsto_nhds {x : Filter β} {a : α} :
    TendstoTendsto f x (𝓝 a) ↔ ∀ ε > (1 : α), ∀ᶠ b in x, |f b / a|ₘ < ε := by
  simp [nhds_eq_iInf_mabs_div, mabs_div_comm a]

Characterization of Convergence via Multiplicative Absolute Value in Ordered Groups

Informal description

Let $\alpha$ be a linearly ordered commutative group with the order topology, and let $f : \beta \to \alpha$ be a function. For any filter $x$ on $\beta$ and any element $a \in \alpha$, the function $f$ tends to $a$ along $x$ if and only if for every $\varepsilon > 1$ in $\alpha$, the set $\{b \in \beta \mid |f(b)/a|_m < \varepsilon\}$ is eventually in $x$.

eventually_mabs_div_lt theorem

(a : α) {ε : α} (hε : 1 < ε) : ∀ᶠ x in 𝓝 a, |x / a|ₘ < ε

Full source

@[to_additive]
theorem eventually_mabs_div_lt (a : α) {ε : α} (hε : 1 < ε) : ∀ᶠ x in 𝓝 a, |x / a|ₘ < ε :=
  (nhds_eq_iInf_mabs_div a).symm ▸
    mem_iInf_of_mem ε (mem_iInf_of_mem hε <| by simp only [mabs_div_comm, mem_principal_self])

Neighborhood Characterization via Multiplicative Absolute Value Inequality

Informal description

Let $\alpha$ be a linearly ordered commutative group with the order topology. For any element $a \in \alpha$ and any $\varepsilon > 1$, there exists a neighborhood of $a$ such that for all $x$ in this neighborhood, the multiplicative absolute value of $x/a$ is less than $\varepsilon$, i.e., $|x/a|_m < \varepsilon$.

Filter.Tendsto.mul_atTop' theorem

{C : α} (hf : Tendsto f l (𝓝 C)) (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atTop

Full source

/-- In a linearly ordered commutative group with the order topology,
if `f` tends to `C` and `g` tends to `atTop` then `f * g` tends to `atTop`. -/
@[to_additive add_atTop "In a linearly ordered additive commutative group with the order topology,
if `f` tends to `C` and `g` tends to `atTop` then `f + g` tends to `atTop`."]
theorem Filter.Tendsto.mul_atTop' {C : α} (hf : Tendsto f l (𝓝 C)) (hg : Tendsto g l atTop) :
    Tendsto (fun x => f x * g x) l atTop := by
  nontriviality α
  obtain ⟨C', hC'⟩ : ∃ C', C' < C := exists_lt C
  refine tendsto_atTop_mul_left_of_le' _ C' ?_ hg
  exact (hf.eventually (lt_mem_nhds hC')).mono fun x => le_of_lt

Product of a Convergent Function and a Function Tending to Infinity Tends to Infinity

Informal description

Let $\alpha$ be a linearly ordered commutative group with the order topology, and let $f$ and $g$ be functions from a filter $l$ to $\alpha$. If $f$ tends to $C$ in the neighborhood filter of $C$ and $g$ tends to $+\infty$, then the product function $f \cdot g$ tends to $+\infty$.

Filter.Tendsto.mul_atBot' theorem

{C : α} (hf : Tendsto f l (𝓝 C)) (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atBot

Full source

/-- In a linearly ordered commutative group with the order topology,
if `f` tends to `C` and `g` tends to `atBot` then `f * g` tends to `atBot`. -/
@[to_additive add_atBot "In a linearly ordered additive commutative group with the order topology,
if `f` tends to `C` and `g` tends to `atBot` then `f + g` tends to `atBot`."]
theorem Filter.Tendsto.mul_atBot' {C : α} (hf : Tendsto f l (𝓝 C)) (hg : Tendsto g l atBot) :
    Tendsto (fun x => f x * g x) l atBot :=
  Filter.Tendsto.mul_atTop' (α := αᵒᵈ) hf hg

Product of a Convergent Function and a Function Tending to Negative Infinity Tends to Negative Infinity

Informal description

Let $\alpha$ be a linearly ordered commutative group with the order topology, and let $f$ and $g$ be functions from a filter $l$ to $\alpha$. If $f$ tends to $C$ in the neighborhood filter of $C$ and $g$ tends to $-\infty$, then the product function $f \cdot g$ tends to $-\infty$.

Filter.Tendsto.atTop_mul' theorem

{C : α} (hf : Tendsto f l atTop) (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atTop

Full source

/-- In a linearly ordered commutative group with the order topology,
 if `f` tends to `atTop` and `g` tends to `C` then `f * g` tends to `atTop`. -/
@[to_additive atTop_add "In a linearly ordered additive commutative group with the order topology,
if `f` tends to `atTop` and `g` tends to `C` then `f + g` tends to `atTop`."]
theorem Filter.Tendsto.atTop_mul' {C : α} (hf : Tendsto f l atTop) (hg : Tendsto g l (𝓝 C)) :
    Tendsto (fun x => f x * g x) l atTop := by
  conv in _ * _ => rw [mul_comm]
  exact hg.mul_atTop' hf

Product of a Function Tending to Infinity and a Convergent Function Tends to Infinity

Informal description

Let $\alpha$ be a linearly ordered commutative group with the order topology, and let $f$ and $g$ be functions from a filter $l$ to $\alpha$. If $f$ tends to $+\infty$ and $g$ tends to $C$ in the neighborhood filter of $C$, then the product function $f \cdot g$ tends to $+\infty$.

Filter.Tendsto.atBot_mul' theorem

{C : α} (hf : Tendsto f l atBot) (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atBot

Full source

/-- In a linearly ordered commutative group with the order topology,
if `f` tends to `atBot` and `g` tends to `C` then `f * g` tends to `atBot`. -/
@[to_additive atBot_add "In a linearly ordered additive commutative group with the order topology,
if `f` tends to `atBot` and `g` tends to `C` then `f + g` tends to `atBot`."]
theorem Filter.Tendsto.atBot_mul' {C : α} (hf : Tendsto f l atBot) (hg : Tendsto g l (𝓝 C)) :
    Tendsto (fun x => f x * g x) l atBot := by
  conv in _ * _ => rw [mul_comm]
  exact hg.mul_atBot' hf

Product of a Function Tending to Negative Infinity and a Convergent Function Tends to Negative Infinity

Informal description

Let $\alpha$ be a linearly ordered commutative group with the order topology, and let $f$ and $g$ be functions from a filter $l$ to $\alpha$. If $f$ tends to $-\infty$ and $g$ tends to $C$ in the neighborhood filter of $C$, then the product function $f \cdot g$ tends to $-\infty$.

nhds_basis_mabs_div_lt theorem

[NoMaxOrder α] (a : α) : (𝓝 a).HasBasis (fun ε : α => (1 : α) < ε) fun ε => {b | |b / a|ₘ < ε}

Full source

@[to_additive]
theorem nhds_basis_mabs_div_lt [NoMaxOrder α] (a : α) :
    (𝓝 a).HasBasis (fun ε : α => (1 : α) < ε) fun ε => { b | |b / a|ₘ < ε } := by
  simp only [nhds_eq_iInf_mabs_div, mabs_div_comm (a := a)]
  refine hasBasis_biInf_principal' (fun x hx y hy => ?_) (exists_gt _)
  exact ⟨min x y, lt_min hx hy, fun _ hz => hz.trans_le (min_le_left _ _),
    fun _ hz => hz.trans_le (min_le_right _ _)⟩

Neighborhood Basis via Multiplicative Absolute Value in Ordered Groups Without Maximal Element

Informal description

Let $\alpha$ be a linearly ordered commutative group with the order topology and no maximal element. For any element $a \in \alpha$, the neighborhood filter $\mathcal{N}(a)$ has a basis consisting of sets of the form $\{b \mid |b/a|_m < \varepsilon\}$ for all $\varepsilon > 1$, where $|\cdot|_m$ denotes the multiplicative absolute value.

nhds_basis_Ioo_one_lt theorem

[NoMaxOrder α] (a : α) : (𝓝 a).HasBasis (fun ε : α => (1 : α) < ε) fun ε => Ioo (a / ε) (a * ε)

Full source

@[to_additive]
theorem nhds_basis_Ioo_one_lt [NoMaxOrder α] (a : α) :
    (𝓝 a).HasBasis (fun ε : α => (1 : α) < ε) fun ε => Ioo (a / ε) (a * ε) := by
  convert nhds_basis_mabs_div_lt a
  simp only [Ioo, mabs_lt, ← div_lt_iff_lt_mul, inv_lt_div_iff_lt_mul, div_lt_comm]

Neighborhood Basis via Open Intervals in Ordered Groups Without Maximal Element

Informal description

Let $\alpha$ be a linearly ordered commutative group with the order topology and no maximal element. For any element $a \in \alpha$, the neighborhood filter $\mathcal{N}(a)$ has a basis consisting of open intervals of the form $(a/\varepsilon, a \cdot \varepsilon)$ for all $\varepsilon > 1$.

nhds_basis_Icc_one_lt theorem

[NoMaxOrder α] [DenselyOrdered α] (a : α) : (𝓝 a).HasBasis ((1 : α) < ·) fun ε ↦ Icc (a / ε) (a * ε)

Full source

@[to_additive]
theorem nhds_basis_Icc_one_lt [NoMaxOrder α] [DenselyOrdered α] (a : α) :
    (𝓝 a).HasBasis ((1 : α) < ·) fun ε ↦ Icc (a / ε) (a * ε) :=
  (nhds_basis_Ioo_one_lt a).to_hasBasis
    (fun _ε ε₁ ↦ let ⟨δ, δ₁, δε⟩ := exists_between ε₁
      ⟨δ, δ₁, Icc_subset_Ioo (by gcongr) (by gcongr)⟩)
    (fun ε ε₁ ↦ ⟨ε, ε₁, Ioo_subset_Icc_self⟩)

Neighborhood Basis via Closed Intervals in Densely Ordered Groups Without Maximal Element

Informal description

Let $\alpha$ be a densely ordered, linearly ordered commutative group with the order topology and no maximal element. For any element $a \in \alpha$, the neighborhood filter $\mathcal{N}(a)$ has a basis consisting of closed intervals of the form $[a/\varepsilon, a \cdot \varepsilon]$ for all $\varepsilon > 1$.

nhds_basis_one_mabs_lt theorem

[NoMaxOrder α] : (𝓝 (1 : α)).HasBasis (fun ε : α => (1 : α) < ε) fun ε => {b | |b|ₘ < ε}

Full source

@[to_additive]
theorem nhds_basis_one_mabs_lt [NoMaxOrder α] :
    (𝓝 (1 : α)).HasBasis (fun ε : α => (1 : α) < ε) fun ε => { b | |b|ₘ < ε } := by
  simpa using nhds_basis_mabs_div_lt (1 : α)

Neighborhood Basis at Identity via Multiplicative Absolute Value in Ordered Groups Without Maximal Element

Informal description

Let $\alpha$ be a linearly ordered commutative group with the order topology and no maximal element. The neighborhood filter $\mathcal{N}(1)$ of the identity element $1 \in \alpha$ has a basis consisting of sets of the form $\{b \mid |b|_m < \varepsilon\}$ for all $\varepsilon > 1$, where $|\cdot|_m$ denotes the multiplicative absolute value.

nhds_basis_Ioo_one_lt_of_one_lt theorem

 [NoMaxOrder α] {a : α} (ha : 1 < a) : (𝓝 a).HasBasis (fun ε : α => (1 : α) < ε ∧ ε ≤ a) fun ε => Ioo (a / ε) (a * ε)

Full source

/-- If `a > 1`, then open intervals `(a / ε, aε)`, `1 < ε ≤ a`,
form a basis of neighborhoods of `a`.

This upper bound for `ε` guarantees that all elements of these intervals are greater than one. -/
@[to_additive "If `a` is positive, then the intervals `(a - ε, a + ε)`, `0 < ε ≤ a`,
form a basis of neighborhoods of `a`.

This upper bound for `ε` guarantees that all elements of these intervals are positive."]
theorem nhds_basis_Ioo_one_lt_of_one_lt [NoMaxOrder α] {a : α} (ha : 1 < a) :
    (𝓝 a).HasBasis (fun ε : α => (1 : α) < ε ∧ ε ≤ a) fun ε => Ioo (a / ε) (a * ε) :=
  (nhds_basis_Ioo_one_lt a).restrict fun ε hε ↦
    ⟨min a ε, lt_min ha hε, min_le_left _ _, by gcongr <;> apply min_le_right⟩

Neighborhood Basis via Open Intervals for Elements Greater Than One in Ordered Groups Without Maximal Element

Informal description

Let $\alpha$ be a linearly ordered commutative group with the order topology and no maximal element. For any element $a \in \alpha$ with $a > 1$, the neighborhood filter $\mathcal{N}(a)$ has a basis consisting of open intervals of the form $(a/\varepsilon, a \cdot \varepsilon)$ for all $\varepsilon$ satisfying $1 < \varepsilon \leq a$.

Set.OrdConnected.mem_nhdsGE theorem

(hS : OrdConnected S) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ 𝓝[≥] x

Full source

/-- If `S` is order-connected and contains two points `x < y`,
then `S` is a right neighbourhood of `x`. -/
lemma mem_nhdsGE (hS : OrdConnected S) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ 𝓝[≥] x :=
  mem_of_superset (Icc_mem_nhdsGE hxy) <| hS.out hx hy

Order-connected sets are right neighborhoods of their points

Informal description

Let $S$ be an order-connected set in a topological space with the order topology, and let $x, y \in S$ with $x < y$. Then $S$ is a right neighborhood of $x$ in the sense that it contains all points sufficiently close to $x$ from the right, i.e., $S \in \mathcal{N}_{\geq x}$.

Set.OrdConnected.mem_nhdsGT theorem

(hS : OrdConnected S) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ 𝓝[>] x

Full source

/-- If `S` is order-connected and contains two points `x < y`,
then `S` is a punctured right neighbourhood of `x`. -/
lemma mem_nhdsGT (hS : OrdConnected S) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ 𝓝[>] x :=
  nhdsWithin_mono _ Ioi_subset_Ici_self <| hS.mem_nhdsGE hx hy hxy

Order-connected sets are punctured right neighborhoods of their points

Informal description

Let $S$ be an order-connected set in a topological space with the order topology, and let $x, y \in S$ with $x < y$. Then $S$ is a punctured right neighborhood of $x$, i.e., it contains all points sufficiently close to $x$ from the right but not equal to $x$, i.e., $S \in \mathcal{N}_{> x}$.

Set.OrdConnected.mem_nhdsLE theorem

(hS : OrdConnected S) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ 𝓝[≤] y

Full source

/-- If `S` is order-connected and contains two points `x < y`, then `S` is a left neighbourhood
of `y`. -/
lemma mem_nhdsLE (hS : OrdConnected S) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ 𝓝[≤] y :=
  hS.dual.mem_nhdsGE hy hx hxy

Order-connected sets are left neighborhoods of their points

Informal description

Let $S$ be an order-connected set in a topological space with the order topology, and let $x, y \in S$ with $x < y$. Then $S$ is a left neighborhood of $y$ in the sense that it contains all points sufficiently close to $y$ from the left, i.e., $S \in \mathcal{N}_{\leq y}$.

Set.OrdConnected.mem_nhdsLT theorem

(hS : OrdConnected S) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ 𝓝[<] y

Full source

/-- If `S` is order-connected and contains two points `x < y`, then `S` is a punctured left
neighbourhood of `y`. -/
lemma mem_nhdsLT (hS : OrdConnected S) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ 𝓝[<] y :=
  hS.dual.mem_nhdsGT hy hx hxy

Order-connected sets are punctured left neighborhoods of their points

Informal description

Let $S$ be an order-connected set in a topological space with the order topology, and let $x, y \in S$ with $x < y$. Then $S$ is a punctured left neighborhood of $y$, i.e., it contains all points sufficiently close to $y$ from the left but not equal to $y$, i.e., $S \in \mathcal{N}_{< y}$.