Mathlib.Topology.Order.Basic

OrderTopology structure

(α : Type*) [t : TopologicalSpace α] [Preorder α]

Full source

/-- The order topology on an ordered type is the topology generated by open intervals. We register
it on a preorder, but it is mostly interesting in linear orders, where it is also order-closed.
We define it as a mixin. If you want to introduce the order topology on a preorder, use
`Preorder.topology`. -/
class OrderTopology (α : Type*) [t : TopologicalSpace α] [Preorder α] : Prop where
  /-- The topology is generated by open intervals `Set.Ioi _` and `Set.Iio _`. -/
  topology_eq_generate_intervals : t = generateFrom { s | ∃ a, s = Ioi a ∨ s = Iio a }

Order Topology Mixin

Informal description

The structure `OrderTopology` is a mixin that asserts that a given topological space structure on a preordered type `α` coincides with the order topology, which is generated by open intervals. This is particularly relevant for linear orders where the topology is also order-closed. To introduce the order topology on a preorder, use `Preorder.topology`.

Preorder.topology definition

(α : Type*) [Preorder α] : TopologicalSpace α

Full source

/-- (Order) topology on a partial order `α` generated by the subbase of open intervals
`(a, ∞) = { x ∣ a < x }, (-∞ , b) = {x ∣ x < b}` for all `a, b` in `α`. We do not register it as an
instance as many ordered sets are already endowed with the same topology, most often in a non-defeq
way though. Register as a local instance when necessary. -/
def Preorder.topology (α : Type*) [Preorder α] : TopologicalSpace α :=
  generateFrom { s : Set α | ∃ a : α, s = { b : α | a < b } ∨ s = { b : α | b < a } }

Order topology on a preorder

Informal description

The order topology on a preorder $\alpha$ is the topology generated by the subbase consisting of all open intervals of the form $(a, \infty) = \{x \mid a < x\}$ and $(-\infty, b) = \{x \mid x < b\}$ for $a, b \in \alpha$. This is not registered as a global instance since many ordered types already have topologies defined in other ways (which may be equal but not definitionally equal to this topology). It can be registered as a local instance when needed.

instOrderTopologyOrderDual instance

[t : OrderTopology α] : OrderTopology αᵒᵈ

Full source

instance [t : OrderTopology α] : OrderTopology αᵒᵈ :=
  ⟨by
    convert OrderTopology.topology_eq_generate_intervals (α := α) using 6
    apply or_comm⟩

Order Topology on Order Dual

Informal description

For any preordered type $\alpha$ equipped with an order topology, the order dual $\alpha^{\mathrm{op}}$ also carries an order topology.

isOpen_iff_generate_intervals theorem

[t : OrderTopology α] {s : Set α} : IsOpen s ↔ GenerateOpen {s | ∃ a, s = Ioi a ∨ s = Iio a} s

Full source

theorem isOpen_iff_generate_intervals [t : OrderTopology α] {s : Set α} :
    IsOpenIsOpen s ↔ GenerateOpen { s | ∃ a, s = Ioi a ∨ s = Iio a } s := by
  rw [t.topology_eq_generate_intervals]; rfl

Characterization of Open Sets in Order Topology via Intervals

Informal description

Let $\alpha$ be a preordered type equipped with an order topology. A subset $s \subseteq \alpha$ is open if and only if it can be generated from the subbase consisting of all sets of the form $(a, \infty)$ or $(-\infty, b)$ for some $a, b \in \alpha$.

isOpen_lt' theorem

[OrderTopology α] (a : α) : IsOpen {b : α | a < b}

Full source

theorem isOpen_lt' [OrderTopology α] (a : α) : IsOpen { b : α | a < b } :=
  isOpen_iff_generate_intervals.2 <| .basic _ ⟨a, .inl rfl⟩

Openness of Upper Set in Order Topology

Informal description

For any element $a$ in a preordered type $\alpha$ equipped with the order topology, the set $\{b \in \alpha \mid a < b\}$ is open.

isOpen_gt' theorem

[OrderTopology α] (a : α) : IsOpen {b : α | b < a}

Full source

theorem isOpen_gt' [OrderTopology α] (a : α) : IsOpen { b : α | b < a } :=
  isOpen_iff_generate_intervals.2 <| .basic _ ⟨a, .inr rfl⟩

Openness of Lower Set in Order Topology

Informal description

For any element $a$ in a preordered type $\alpha$ equipped with the order topology, the set $\{b \in \alpha \mid b < a\}$ is open.

lt_mem_nhds theorem

[OrderTopology α] {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 b, a < x

Full source

theorem lt_mem_nhds [OrderTopology α] {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 b, a < x :=
  (isOpen_lt' _).mem_nhds h

Neighborhood of $b$ contains points greater than $a$ when $a < b$ in order topology

Informal description

For any elements $a$ and $b$ in a preordered type $\alpha$ equipped with the order topology, if $a < b$, then the set $\{x \in \alpha \mid a < x\}$ is a neighborhood of $b$.

le_mem_nhds theorem

[OrderTopology α] {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 b, a ≤ x

Full source

theorem le_mem_nhds [OrderTopology α] {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 b, a ≤ x :=
  (lt_mem_nhds h).mono fun _ => le_of_lt

Neighborhood of $b$ contains points greater than or equal to $a$ when $a < b$ in order topology

Informal description

For any elements $a$ and $b$ in a preordered type $\alpha$ equipped with the order topology, if $a < b$, then the set $\{x \in \alpha \mid a \leq x\}$ is a neighborhood of $b$.

gt_mem_nhds theorem

[OrderTopology α] {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 a, x < b

Full source

theorem gt_mem_nhds [OrderTopology α] {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 a, x < b :=
  (isOpen_gt' _).mem_nhds h

Neighborhood of $a$ contains points less than $b$ when $a < b$ in order topology

Informal description

For any elements $a$ and $b$ in a preordered type $\alpha$ equipped with the order topology, if $a < b$, then the set $\{x \in \alpha \mid x < b\}$ is a neighborhood of $a$.

ge_mem_nhds theorem

[OrderTopology α] {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 a, x ≤ b

Full source

theorem ge_mem_nhds [OrderTopology α] {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 a, x ≤ b :=
  (gt_mem_nhds h).mono fun _ => le_of_lt

Neighborhood of $a$ contains points less than or equal to $b$ when $a < b$ in order topology

Informal description

For any elements $a$ and $b$ in a preordered type $\alpha$ equipped with the order topology, if $a < b$, then the set $\{x \in \alpha \mid x \leq b\}$ is a neighborhood of $a$.

nhds_eq_order theorem

[OrderTopology α] (a : α) : 𝓝 a = (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)

Full source

theorem nhds_eq_order [OrderTopology α] (a : α) :
    𝓝 a = (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b) := by
  rw [OrderTopology.topology_eq_generate_intervals (α := α), nhds_generateFrom]
  simp_rw [mem_setOf_eq, @and_comm (a ∈ _), exists_or, or_and_right, iInf_or, iInf_and,
    iInf_exists, iInf_inf_eq, iInf_comm (ι := Set α), iInf_iInf_eq_left, mem_Ioi, mem_Iio]

Characterization of Neighborhood Filter in Order Topology

Informal description

Let $\alpha$ be a topological space with a preorder structure and the order topology. For any element $a \in \alpha$, the neighborhood filter $\mathcal{N}(a)$ is equal to the infimum of the principal filters generated by the sets $(b, \infty)$ for all $b < a$ and $(-\infty, b)$ for all $b > a$. In other words, \[ \mathcal{N}(a) = \left( \bigwedge_{b < a} \mathcal{P}((b, \infty)) \right) \sqcap \left( \bigwedge_{b > a} \mathcal{P}((-\infty, b)) \right). \]

tendsto_order theorem

 [OrderTopology α] {f : β → α} {a : α} {x : Filter β} :
  Tendsto f x (𝓝 a) ↔ (∀ a' < a, ∀ᶠ b in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ b in x, f b < a'

Full source

theorem tendsto_order [OrderTopology α] {f : β → α} {a : α} {x : Filter β} :
    TendstoTendsto f x (𝓝 a) ↔ (∀ a' < a, ∀ᶠ b in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ b in x, f b < a' := by
  simp only [nhds_eq_order a, tendsto_inf, tendsto_iInf, tendsto_principal]; rfl

Characterization of Convergence in Order Topology via One-Sided Limits

Informal description

Let $\alpha$ be a topological space with an order topology, $f : \beta \to \alpha$ a function, $a \in \alpha$, and $x$ a filter on $\beta$. Then the function $f$ tends to $a$ along the filter $x$ if and only if for every $a' < a$, the set $\{b \mid a' < f b\}$ is eventually in $x$, and for every $a'' > a$, the set $\{b \mid f b < a''\}$ is eventually in $x$. In other words, $f \to a$ along $x$ if and only if: 1. For all $a' < a$, $f(b) > a'$ eventually as $b \to x$. 2. For all $a'' > a$, $f(b) < a''$ eventually as $b \to x$.

tendstoIccClassNhds instance

[OrderTopology α] (a : α) : TendstoIxxClass Icc (𝓝 a) (𝓝 a)

Full source

instance tendstoIccClassNhds [OrderTopology α] (a : α) : TendstoIxxClass Icc (𝓝 a) (𝓝 a) := by
  simp only [nhds_eq_order, iInf_subtype']
  refine
    ((hasBasis_iInf_principal_finite _).inf (hasBasis_iInf_principal_finite _)).tendstoIxxClass
      fun s _ => ?_
  refine ((ordConnected_biInter ?_).inter (ordConnected_biInter ?_)).out <;> intro _ _
  exacts [ordConnected_Ioi, ordConnected_Iio]

Compatibility of Closed Intervals with Neighborhood Filters in Order Topology

Informal description

For any topological space $\alpha$ with an order topology and any element $a \in \alpha$, the closed interval operation $\operatorname{Icc}$ is compatible with the neighborhood filter $\mathcal{N}(a)$. This means that for any two functions $f, g$ converging to $a$ in $\mathcal{N}(a)$, the set of points where $f$ and $g$ lie within the closed interval $\operatorname{Icc}(f, g)$ also converges to $a$.

tendstoIcoClassNhds instance

[OrderTopology α] (a : α) : TendstoIxxClass Ico (𝓝 a) (𝓝 a)

Full source

instance tendstoIcoClassNhds [OrderTopology α] (a : α) : TendstoIxxClass Ico (𝓝 a) (𝓝 a) :=
  tendstoIxxClass_of_subset fun _ _ => Ico_subset_Icc_self

Compatibility of Left-Closed Right-Open Intervals with Neighborhood Filters in Order Topology

Informal description

For any topological space $\alpha$ with an order topology and any element $a \in \alpha$, the left-closed right-open interval operation $\operatorname{Ico}$ is compatible with the neighborhood filter $\mathcal{N}(a)$. This means that for any two functions $f, g$ converging to $a$ in $\mathcal{N}(a)$, the set of points where $f$ and $g$ lie within the interval $\operatorname{Ico}(f, g)$ also converges to $a$.

tendstoIocClassNhds instance

[OrderTopology α] (a : α) : TendstoIxxClass Ioc (𝓝 a) (𝓝 a)

Full source

instance tendstoIocClassNhds [OrderTopology α] (a : α) : TendstoIxxClass Ioc (𝓝 a) (𝓝 a) :=
  tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self

Compatibility of Left-Open Right-Closed Intervals with Neighborhood Filters in Order Topology

Informal description

For any topological space $\alpha$ with an order topology and any element $a \in \alpha$, the left-open right-closed interval operation $\operatorname{Ioc}$ is compatible with the neighborhood filter $\mathcal{N}(a)$. This means that for any two functions $f, g$ converging to $a$ in $\mathcal{N}(a)$, the set of points where $f$ and $g$ lie within the interval $\operatorname{Ioc}(f, g)$ also converges to $a$.

tendstoIooClassNhds instance

[OrderTopology α] (a : α) : TendstoIxxClass Ioo (𝓝 a) (𝓝 a)

Full source

instance tendstoIooClassNhds [OrderTopology α] (a : α) : TendstoIxxClass Ioo (𝓝 a) (𝓝 a) :=
  tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Icc_self

Compatibility of Open Intervals with Neighborhood Filters in Order Topology

Informal description

For any topological space $\alpha$ with an order topology and any element $a \in \alpha$, the open interval operation $\operatorname{Ioo}$ is compatible with the neighborhood filter $\mathcal{N}(a)$. This means that for any two functions $f, g$ converging to $a$ in $\mathcal{N}(a)$, the set of points where $f$ and $g$ lie within the open interval $\operatorname{Ioo}(f, g)$ also converges to $a$.

tendsto_of_tendsto_of_tendsto_of_le_of_le' theorem

 [OrderTopology α] {f g h : β → α} {b : Filter β} {a : α} (hg : Tendsto g b (𝓝 a)) (hh : Tendsto h b (𝓝 a))
  (hgf : ∀ᶠ b in b, g b ≤ f b) (hfh : ∀ᶠ b in b, f b ≤ h b) : Tendsto f b (𝓝 a)

Full source

/-- **Squeeze theorem** (also known as **sandwich theorem**). This version assumes that inequalities
hold eventually for the filter. -/
theorem tendsto_of_tendsto_of_tendsto_of_le_of_le' [OrderTopology α] {f g h : β → α} {b : Filter β}
    {a : α} (hg : Tendsto g b (𝓝 a)) (hh : Tendsto h b (𝓝 a)) (hgf : ∀ᶠ b in b, g b ≤ f b)
    (hfh : ∀ᶠ b in b, f b ≤ h b) : Tendsto f b (𝓝 a) :=
  (hg.Icc hh).of_smallSets <| hgf.and hfh

Squeeze theorem for order topologies (eventual version)

Informal description

Let $\alpha$ be a topological space with an order topology, and let $f, g, h : \beta \to \alpha$ be functions. Suppose $g$ and $h$ both tend to $a \in \alpha$ along a filter $b$ on $\beta$. If eventually $g(b) \leq f(b) \leq h(b)$ for all $b \in \beta$, then $f$ also tends to $a$ along $b$.

tendsto_of_tendsto_of_tendsto_of_le_of_le theorem

 [OrderTopology α] {f g h : β → α} {b : Filter β} {a : α} (hg : Tendsto g b (𝓝 a)) (hh : Tendsto h b (𝓝 a))
  (hgf : g ≤ f) (hfh : f ≤ h) : Tendsto f b (𝓝 a)

Full source

/-- **Squeeze theorem** (also known as **sandwich theorem**). This version assumes that inequalities
hold everywhere. -/
theorem tendsto_of_tendsto_of_tendsto_of_le_of_le [OrderTopology α] {f g h : β → α} {b : Filter β}
    {a : α} (hg : Tendsto g b (𝓝 a)) (hh : Tendsto h b (𝓝 a)) (hgf : g ≤ f) (hfh : f ≤ h) :
    Tendsto f b (𝓝 a) :=
  tendsto_of_tendsto_of_tendsto_of_le_of_le' hg hh (Eventually.of_forall hgf)
    (Eventually.of_forall hfh)

Squeeze Theorem for Order Topologies (Pointwise Version)

Informal description

Let $\alpha$ be a topological space with an order topology, and let $f, g, h : \beta \to \alpha$ be functions. If $g$ and $h$ both converge to $a \in \alpha$ along a filter $b$ on $\beta$, and $g(b) \leq f(b) \leq h(b)$ holds for all $b \in \beta$, then $f$ also converges to $a$ along $b$.

nhds_order_unbounded theorem

 [OrderTopology α] {a : α} (hu : ∃ u, a < u) (hl : ∃ l, l < a) : 𝓝 a = ⨅ (l) (_ : l < a) (u) (_ : a < u), 𝓟 (Ioo l u)

Full source

theorem nhds_order_unbounded [OrderTopology α] {a : α} (hu : ∃ u, a < u) (hl : ∃ l, l < a) :
    𝓝 a = ⨅ (l) (_ : l < a) (u) (_ : a < u), 𝓟 (Ioo l u) := by
  simp only [nhds_eq_order, ← inf_biInf, ← biInf_inf, *, ← inf_principal, ← Ioi_inter_Iio]; rfl

Characterization of Neighborhood Filter via Open Intervals in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology and $a \in \alpha$. If there exist elements $u$ and $l$ such that $l < a < u$, then the neighborhood filter $\mathcal{N}(a)$ is equal to the infimum of the principal filters generated by the open intervals $(l, u)$ for all $l < a$ and $u > a$. In other words, \[ \mathcal{N}(a) = \bigwedge_{\substack{l < a \\ u > a}} \mathcal{P}((l, u)). \]

tendsto_order_unbounded theorem

 [OrderTopology α] {f : β → α} {a : α} {x : Filter β} (hu : ∃ u, a < u) (hl : ∃ l, l < a)
  (h : ∀ l u, l < a → a < u → ∀ᶠ b in x, l < f b ∧ f b < u) : Tendsto f x (𝓝 a)

Full source

theorem tendsto_order_unbounded [OrderTopology α] {f : β → α} {a : α} {x : Filter β}
    (hu : ∃ u, a < u) (hl : ∃ l, l < a) (h : ∀ l u, l < a → a < u → ∀ᶠ b in x, l < f b ∧ f b < u) :
    Tendsto f x (𝓝 a) := by
  simp only [nhds_order_unbounded hu hl, tendsto_iInf, tendsto_principal]
  exact fun l hl u => h l u hl

Unbounded Order Topology Limit Characterization

Informal description

Let $\alpha$ be a topological space with an order topology, and let $f \colon \beta \to \alpha$ be a function. Suppose there exist elements $u$ and $l$ in $\alpha$ such that $l < a < u$. If for every $l < a$ and $u > a$, the function $f$ eventually satisfies $l < f(b) < u$ for all $b$ in the filter $x$, then $f$ tends to $a$ along the filter $x$, i.e., $\lim_{x} f = a$.

tendstoIxxNhdsWithin instance

 {α : Type*} [TopologicalSpace α] (a : α) {s t : Set α} {Ixx} [TendstoIxxClass Ixx (𝓝 a) (𝓝 a)]
  [TendstoIxxClass Ixx (𝓟 s) (𝓟 t)] : TendstoIxxClass Ixx (𝓝[s] a) (𝓝[t] a)

Full source

instance tendstoIxxNhdsWithin {α : Type*} [TopologicalSpace α] (a : α) {s t : Set α}
    {Ixx} [TendstoIxxClass Ixx (𝓝 a) (𝓝 a)] [TendstoIxxClass Ixx (𝓟 s) (𝓟 t)] :
    TendstoIxxClass Ixx (𝓝[s] a) (𝓝[t] a) :=
  Filter.tendstoIxxClass_inf

Preservation of Interval Convergence in Relative Neighborhoods

Informal description

For a topological space $\alpha$ with a point $a \in \alpha$ and subsets $s, t \subseteq \alpha$, if the interval operation `Ixx` preserves convergence in the neighborhoods of $a$ and in the principal filters of $s$ and $t$, then `Ixx` also preserves convergence in the neighborhoods of $a$ within $s$ and $t$.

tendstoIccClassNhdsPi instance

 {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, TopologicalSpace (α i)] [∀ i, OrderTopology (α i)]
  (f : ∀ i, α i) : TendstoIxxClass Icc (𝓝 f) (𝓝 f)

Full source

instance tendstoIccClassNhdsPi {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)]
    [∀ i, TopologicalSpace (α i)] [∀ i, OrderTopology (α i)] (f : ∀ i, α i) :
    TendstoIxxClass Icc (𝓝 f) (𝓝 f) := by
  constructor
  conv in (𝓝 f).smallSets => rw [nhds_pi, Filter.pi]
  simp only [smallSets_iInf, smallSets_comap_eq_comap_image, tendsto_iInf, tendsto_comap_iff]
  intro i
  have : Tendsto (fun g : ∀ i, α i => g i) (𝓝 f) (𝓝 (f i)) := (continuous_apply i).tendsto f
  refine (this.comp tendsto_fst).Icc (this.comp tendsto_snd) |>.smallSets_mono ?_
  filter_upwards [] using fun ⟨f, g⟩ ↦ image_subset_iff.mpr fun p hp ↦ ⟨hp.1 i, hp.2 i⟩

Compatibility of Closed Intervals with Neighborhood Filters in Product of Ordered Topological Spaces

Informal description

For any family of preordered topological spaces $\{ \alpha_i \}_{i \in \iota}$ where each $\alpha_i$ is equipped with the order topology, and for any function $f \in \prod_{i} \alpha_i$, the closed interval operation $\operatorname{Icc}$ is compatible with the neighborhood filter $\mathcal{N}(f)$. This means that for any two functions $g, h$ converging to $f$ in $\mathcal{N}(f)$, the set of points where $g$ and $h$ lie within the closed interval $\operatorname{Icc}(g, h)$ also converges to $f$.

induced_topology_le_preorder theorem

 [Preorder α] [Preorder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : ∀ {x y}, f x < f y ↔ x < y) :
  induced f ‹TopologicalSpace β› ≤ Preorder.topology α

Full source

theorem induced_topology_le_preorder [Preorder α] [Preorder β] [TopologicalSpace β]
    [OrderTopology β] {f : α → β} (hf : ∀ {x y}, f x < f y ↔ x < y) :
    induced f ‹TopologicalSpace β› ≤ Preorder.topology α := by
  let _ := Preorder.topology α; have : OrderTopology α := ⟨rfl⟩
  refine le_of_nhds_le_nhds fun x => ?_
  simp only [nhds_eq_order, nhds_induced, comap_inf, comap_iInf, comap_principal, Ioi, Iio, ← hf]
  refine inf_le_inf (le_iInf₂ fun a ha => ?_) (le_iInf₂ fun a ha => ?_)
  exacts [iInf₂_le (f a) ha, iInf₂_le (f a) ha]

Induced Topology is Coarser than Order Topology under Order-Embedding

Informal description

Let $\alpha$ and $\beta$ be preordered sets, with $\beta$ equipped with a topological space structure that is the order topology. Given a function $f \colon \alpha \to \beta$ such that for all $x, y \in \alpha$, $f(x) < f(y)$ if and only if $x < y$, the topology on $\alpha$ induced by $f$ is coarser than the order topology on $\alpha$. In other words, the induced topology is contained in the order topology.

induced_topology_eq_preorder theorem

 [Preorder α] [Preorder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : ∀ {x y}, f x < f y ↔ x < y)
  (H₁ : ∀ {a b x}, b < f a → ¬(b < f x) → ∃ y, y < a ∧ b ≤ f y)
  (H₂ : ∀ {a b x}, f a < b → ¬(f x < b) → ∃ y, a < y ∧ f y ≤ b) : induced f ‹TopologicalSpace β› = Preorder.topology α

Full source

theorem induced_topology_eq_preorder [Preorder α] [Preorder β] [TopologicalSpace β]
    [OrderTopology β] {f : α → β} (hf : ∀ {x y}, f x < f y ↔ x < y)
    (H₁ : ∀ {a b x}, b < f a → ¬(b < f x) → ∃ y, y < a ∧ b ≤ f y)
    (H₂ : ∀ {a b x}, f a < b → ¬(f x < b) → ∃ y, a < y ∧ f y ≤ b) :
    induced f ‹TopologicalSpace β› = Preorder.topology α := by
  let _ := Preorder.topology α; have : OrderTopology α := ⟨rfl⟩
  refine le_antisymm (induced_topology_le_preorder hf) ?_
  refine le_of_nhds_le_nhds fun a => ?_
  simp only [nhds_eq_order, nhds_induced, comap_inf, comap_iInf, comap_principal]
  refine inf_le_inf (le_iInf₂ fun b hb => ?_) (le_iInf₂ fun b hb => ?_)
  · rcases em (∃ x, ¬(b < f x)) with (⟨x, hx⟩ | hb)
    · rcases H₁ hb hx with ⟨y, hya, hyb⟩
      exact iInf₂_le_of_le y hya (principal_mono.2 fun z hz => hyb.trans_lt (hf.2 hz))
    · push_neg at hb
      exact le_principal_iff.2 (univ_mem' hb)
  · rcases em (∃ x, ¬(f x < b)) with (⟨x, hx⟩ | hb)
    · rcases H₂ hb hx with ⟨y, hya, hyb⟩
      exact iInf₂_le_of_le y hya (principal_mono.2 fun z hz => (hf.2 hz).trans_le hyb)
    · push_neg at hb
      exact le_principal_iff.2 (univ_mem' hb)

Equality of Induced Topology and Order Topology under Order-Embedding with Boundary Conditions

Informal description

Let $\alpha$ and $\beta$ be preordered sets, with $\beta$ equipped with a topological space structure that is the order topology. Given a function $f \colon \alpha \to \beta$ that is an order embedding (i.e., for all $x, y \in \alpha$, $f(x) < f(y)$ if and only if $x < y$), and satisfying the following additional conditions: 1. For any $a \in \alpha$ and $b, x \in \beta$, if $b < f(a)$ and $b \not< f(x)$, then there exists $y < a$ such that $b \leq f(y)$. 2. For any $a \in \alpha$ and $b, x \in \beta$, if $f(a) < b$ and $f(x) \not< b$, then there exists $y > a$ such that $f(y) \leq b$. Then the topology on $\alpha$ induced by $f$ is equal to the order topology on $\alpha$.

induced_orderTopology' theorem

 {α : Type u} {β : Type v} [Preorder α] [ta : TopologicalSpace β] [Preorder β] [OrderTopology β] (f : α → β)
  (hf : ∀ {x y}, f x < f y ↔ x < y) (H₁ : ∀ {a x}, x < f a → ∃ b < a, x ≤ f b)
  (H₂ : ∀ {a x}, f a < x → ∃ b > a, f b ≤ x) : @OrderTopology _ (induced f ta) _

Full source

theorem induced_orderTopology' {α : Type u} {β : Type v} [Preorder α] [ta : TopologicalSpace β]
    [Preorder β] [OrderTopology β] (f : α → β) (hf : ∀ {x y}, f x < f y ↔ x < y)
    (H₁ : ∀ {a x}, x < f a → ∃ b < a, x ≤ f b) (H₂ : ∀ {a x}, f a < x → ∃ b > a, f b ≤ x) :
    @OrderTopology _ (induced f ta) _ :=
  let _ := induced f ta
  ⟨induced_topology_eq_preorder hf (fun h _ => H₁ h) (fun h _ => H₂ h)⟩

Order Topology Induced by Order-Embedding with Boundary Conditions

Informal description

Let $\alpha$ and $\beta$ be preordered sets, with $\beta$ equipped with a topological space structure that is the order topology. Given a function $f \colon \alpha \to \beta$ such that for all $x, y \in \alpha$, $f(x) < f(y)$ if and only if $x < y$, and satisfying the following conditions: 1. For any $a \in \alpha$ and $x \in \beta$, if $x < f(a)$, then there exists $b < a$ such that $x \leq f(b)$. 2. For any $a \in \alpha$ and $x \in \beta$, if $f(a) < x$, then there exists $b > a$ such that $f(b) \leq x$. Then the topology on $\alpha$ induced by $f$ is the order topology on $\alpha$.

induced_orderTopology theorem

 {α : Type u} {β : Type v} [Preorder α] [ta : TopologicalSpace β] [Preorder β] [OrderTopology β] (f : α → β)
  (hf : ∀ {x y}, f x < f y ↔ x < y) (H : ∀ {x y}, x < y → ∃ a, x < f a ∧ f a < y) : @OrderTopology _ (induced f ta) _

Full source

theorem induced_orderTopology {α : Type u} {β : Type v} [Preorder α] [ta : TopologicalSpace β]
    [Preorder β] [OrderTopology β] (f : α → β) (hf : ∀ {x y}, f x < f y ↔ x < y)
    (H : ∀ {x y}, x < y → ∃ a, x < f a ∧ f a < y) : @OrderTopology _ (induced f ta) _ :=
  induced_orderTopology' f (hf)
    (fun xa => let ⟨b, xb, ba⟩ := H xa; ⟨b, hf.1 ba, le_of_lt xb⟩)
    fun ax => let ⟨b, ab, bx⟩ := H ax; ⟨b, hf.1 ab, le_of_lt bx⟩

Order Topology Induced by Order-Embedding with Intermediate Value Condition

Informal description

Let $\alpha$ and $\beta$ be preordered sets, with $\beta$ equipped with a topological space structure that is the order topology. Given a function $f \colon \alpha \to \beta$ such that for all $x, y \in \alpha$, $f(x) < f(y)$ if and only if $x < y$, and satisfying the following condition: - For any $x, y \in \beta$ with $x < y$, there exists $a \in \alpha$ such that $x < f(a) < y$. Then the topology on $\alpha$ induced by $f$ is the order topology on $\alpha$.

StrictMono.induced_topology_eq_preorder theorem

 {α β : Type*} [LinearOrder α] [LinearOrder β] [t : TopologicalSpace β] [OrderTopology β] {f : α → β}
  (hf : StrictMono f) (hc : OrdConnected (range f)) : t.induced f = Preorder.topology α

Full source

/-- The topology induced by a strictly monotone function with order-connected range is the preorder
topology. -/
nonrec theorem StrictMono.induced_topology_eq_preorder {α β : Type*} [LinearOrder α]
    [LinearOrder β] [t : TopologicalSpace β] [OrderTopology β] {f : α → β}
    (hf : StrictMono f) (hc : OrdConnected (range f)) : t.induced f = Preorder.topology α := by
  refine induced_topology_eq_preorder hf.lt_iff_lt (fun h₁ h₂ => ?_) fun h₁ h₂ => ?_
  · rcases hc.out (mem_range_self _) (mem_range_self _) ⟨not_lt.1 h₂, h₁.le⟩ with ⟨y, rfl⟩
    exact ⟨y, hf.lt_iff_lt.1 h₁, le_rfl⟩
  · rcases hc.out (mem_range_self _) (mem_range_self _) ⟨h₁.le, not_lt.1 h₂⟩ with ⟨y, rfl⟩
    exact ⟨y, hf.lt_iff_lt.1 h₁, le_rfl⟩

Induced Topology Equals Order Topology for Strictly Monotone Functions with Order-Connected Range

Informal description

Let $\alpha$ and $\beta$ be linearly ordered sets, with $\beta$ equipped with the order topology. Given a strictly monotone function $f \colon \alpha \to \beta$ whose range is order-connected, the topology on $\alpha$ induced by $f$ coincides with the order topology on $\alpha$.

StrictMono.isEmbedding_of_ordConnected theorem

 {α β : Type*} [LinearOrder α] [LinearOrder β] [TopologicalSpace α] [h : OrderTopology α] [TopologicalSpace β]
  [OrderTopology β] {f : α → β} (hf : StrictMono f) (hc : OrdConnected (range f)) : IsEmbedding f

Full source

/-- A strictly monotone function between linear orders with order topology is a topological
embedding provided that the range of `f` is order-connected. -/
theorem StrictMono.isEmbedding_of_ordConnected {α β : Type*} [LinearOrder α] [LinearOrder β]
    [TopologicalSpace α] [h : OrderTopology α] [TopologicalSpace β] [OrderTopology β] {f : α → β}
    (hf : StrictMono f) (hc : OrdConnected (range f)) : IsEmbedding f :=
  ⟨⟨h.1.trans <| Eq.symm <| hf.induced_topology_eq_preorder hc⟩, hf.injective⟩

Strictly Monotone Functions with Order-Connected Range are Topological Embeddings

Informal description

Let $\alpha$ and $\beta$ be linearly ordered sets equipped with order topologies. Given a strictly monotone function $f \colon \alpha \to \beta$ whose range is order-connected, $f$ is a topological embedding.

orderTopology_of_ordConnected instance

 {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {t : Set α} [ht : OrdConnected t] : OrderTopology t

Full source

/-- On a `Set.OrdConnected` subset of a linear order, the order topology for the restriction of the
order is the same as the restriction to the subset of the order topology. -/
instance orderTopology_of_ordConnected {α : Type u} [TopologicalSpace α] [LinearOrder α]
    [OrderTopology α] {t : Set α} [ht : OrdConnected t] : OrderTopology t :=
  ⟨(Subtype.strictMono_coe t).induced_topology_eq_preorder <| by
    rwa [← @Subtype.range_val _ t] at ht⟩

Order Topology on Order-Connected Subsets

Informal description

For any linearly ordered topological space $\alpha$ with the order topology, and any order-connected subset $t \subseteq \alpha$, the subspace topology on $t$ coincides with the order topology induced by the restriction of the order to $t$.

nhdsGE_eq_iInf_inf_principal theorem

 [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) : 𝓝[≥] a = (⨅ (u) (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)

Full source

theorem nhdsGE_eq_iInf_inf_principal [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
    𝓝[≥] a = (⨅ (u) (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a) := by
  rw [nhdsWithin, nhds_eq_order]
  refine le_antisymm (inf_le_inf_right _ inf_le_right) (le_inf (le_inf ?_ inf_le_left) inf_le_right)
  exact inf_le_right.trans (le_iInf₂ fun l hl => principal_mono.2 <| Ici_subset_Ioi.2 hl)

Characterization of Neighborhood Filter in Upper Closure Subspace

Informal description

Let $\alpha$ be a topological space with a preorder structure and the order topology. For any element $a \in \alpha$, the neighborhood filter $\mathcal{N}_{\geq}(a)$ of $a$ in the subspace topology on $\{x \mid x \geq a\}$ is equal to the infimum of the principal filters generated by the sets $(-\infty, u)$ for all $u > a$, intersected with the principal filter generated by $[a, \infty)$. In other words, \[ \mathcal{N}_{\geq}(a) = \left( \bigwedge_{u > a} \mathcal{P}((-\infty, u)) \right) \sqcap \mathcal{P}([a, \infty)). \]

nhdsLE_eq_iInf_inf_principal theorem

 [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) : 𝓝[≤] a = (⨅ l < a, 𝓟 (Ioi l)) ⊓ 𝓟 (Iic a)

Full source

theorem nhdsLE_eq_iInf_inf_principal [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
    𝓝[≤] a = (⨅ l < a, 𝓟 (Ioi l)) ⊓ 𝓟 (Iic a) :=
  nhdsGE_eq_iInf_inf_principal (toDual a)

Characterization of Neighborhood Filter in Lower Closure Subspace

Informal description

Let $\alpha$ be a topological space with a preorder structure and the order topology. For any element $a \in \alpha$, the neighborhood filter $\mathcal{N}_{\leq}(a)$ of $a$ in the subspace topology on $\{x \mid x \leq a\}$ is equal to the infimum of the principal filters generated by the sets $(l, \infty)$ for all $l < a$, intersected with the principal filter generated by $(-\infty, a]$. In other words, \[ \mathcal{N}_{\leq}(a) = \left( \bigwedge_{l < a} \mathcal{P}((l, \infty)) \right) \sqcap \mathcal{P}((-\infty, a]). \]

nhdsGE_eq_iInf_principal theorem

 [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} (ha : ∃ u, a < u) : 𝓝[≥] a = ⨅ (u) (_ : a < u), 𝓟 (Ico a u)

Full source

theorem nhdsGE_eq_iInf_principal [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α}
    (ha : ∃ u, a < u) : 𝓝[≥] a = ⨅ (u) (_ : a < u), 𝓟 (Ico a u) := by
  simp only [nhdsGE_eq_iInf_inf_principal, biInf_inf ha, inf_principal, Iio_inter_Ici]

Neighborhood Filter Characterization in Upper Closure Subspace via Infimum of Principal Filters on $[a, u)$ Intervals

Informal description

Let $\alpha$ be a topological space with a preorder structure and the order topology. For any element $a \in \alpha$ such that there exists $u$ with $a < u$, the neighborhood filter $\mathcal{N}_{\geq}(a)$ of $a$ in the subspace topology on $\{x \mid x \geq a\}$ is equal to the infimum of the principal filters generated by the intervals $[a, u)$ for all $u > a$. In other words, \[ \mathcal{N}_{\geq}(a) = \bigwedge_{u > a} \mathcal{P}([a, u)). \]

nhdsLE_eq_iInf_principal theorem

 [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} (ha : ∃ l, l < a) : 𝓝[≤] a = ⨅ l < a, 𝓟 (Ioc l a)

Full source

theorem nhdsLE_eq_iInf_principal [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α}
    (ha : ∃ l, l < a) : 𝓝[≤] a = ⨅ l < a, 𝓟 (Ioc l a) := by
  simp only [nhdsLE_eq_iInf_inf_principal, biInf_inf ha, inf_principal, Ioi_inter_Iic]

Neighborhood Filter Characterization in Lower Closure Subspace via Infimum of Principal Filters on $(l, a]$ Intervals

Informal description

Let $\alpha$ be a topological space with a preorder structure and the order topology. For any element $a \in \alpha$ such that there exists $l$ with $l < a$, the neighborhood filter $\mathcal{N}_{\leq}(a)$ of $a$ in the subspace topology on $\{x \mid x \leq a\}$ is equal to the infimum of the principal filters generated by the intervals $(l, a]$ for all $l < a$. In other words, \[ \mathcal{N}_{\leq}(a) = \bigwedge_{l < a} \mathcal{P}((l, a]). \]

nhdsGE_basis_of_exists_gt theorem

 [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (ha : ∃ u, a < u) :
  (𝓝[≥] a).HasBasis (fun u => a < u) fun u => Ico a u

Full source

theorem nhdsGE_basis_of_exists_gt [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α}
    (ha : ∃ u, a < u) : (𝓝[≥] a).HasBasis (fun u => a < u) fun u => Ico a u :=
  (nhdsGE_eq_iInf_principal ha).symm ▸
    hasBasis_biInf_principal
      (fun b hb c hc => ⟨min b c, lt_min hb hc, Ico_subset_Ico_right (min_le_left _ _),
        Ico_subset_Ico_right (min_le_right _ _)⟩)
      ha

Basis Characterization of Upper Neighborhood Filter via $[a, u)$ Intervals

Informal description

Let $\alpha$ be a topological space with a linear order and the order topology. For any element $a \in \alpha$ such that there exists $u$ with $a < u$, the neighborhood filter $\mathcal{N}_{\geq}(a)$ of $a$ in the subspace topology on $\{x \mid x \geq a\}$ has a basis consisting of the left-closed right-open intervals $[a, u)$ for all $u > a$. In other words, the filter $\mathcal{N}_{\geq}(a)$ is generated by the sets $[a, u)$ where $u$ ranges over all elements greater than $a$.

nhdsLE_basis_of_exists_lt theorem

 [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (ha : ∃ l, l < a) :
  (𝓝[≤] a).HasBasis (fun l => l < a) fun l => Ioc l a

Full source

theorem nhdsLE_basis_of_exists_lt [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α}
    (ha : ∃ l, l < a) : (𝓝[≤] a).HasBasis (fun l => l < a) fun l => Ioc l a := by
  convert nhdsGE_basis_of_exists_gt (α := αᵒᵈ) ha using 2
  exact Ico_toDual.symm

Basis Characterization of Lower Neighborhood Filter via $(l, a]$ Intervals

Informal description

Let $\alpha$ be a topological space with a linear order and the order topology. For any element $a \in \alpha$ such that there exists $l$ with $l < a$, the neighborhood filter $\mathcal{N}_{\leq}(a)$ of $a$ in the subspace topology on $\{x \mid x \leq a\}$ has a basis consisting of the left-open right-closed intervals $(l, a]$ for all $l < a$.

nhdsGE_basis theorem

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

Full source

theorem nhdsGE_basis [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α) :
    (𝓝[≥] a).HasBasis (fun u => a < u) fun u => Ico a u :=
  nhdsGE_basis_of_exists_gt (exists_gt a)

Basis of Upper Neighborhood Filter via $[a, u)$ Intervals in Order Topology without Maximal Element

Informal description

Let $\alpha$ be a topological space with a linear order and the order topology, and assume $\alpha$ has no maximal element. For any element $a \in \alpha$, the neighborhood filter $\mathcal{N}_{\geq}(a)$ of $a$ in the subspace topology on $\{x \mid x \geq a\}$ has a basis consisting of the left-closed right-open intervals $[a, u)$ for all $u > a$.

nhdsLE_basis theorem

 [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] (a : α) :
  (𝓝[≤] a).HasBasis (fun l => l < a) fun l => Ioc l a

Full source

theorem nhdsLE_basis [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] (a : α) :
    (𝓝[≤] a).HasBasis (fun l => l < a) fun l => Ioc l a :=
  nhdsLE_basis_of_exists_lt (exists_lt a)

Basis of Lower Neighborhood Filter via $(l, a]$ Intervals in Order Topology without Minimal Element

Informal description

Let $\alpha$ be a topological space with a linear order and the order topology, and assume $\alpha$ has no minimal element. For any element $a \in \alpha$, the neighborhood filter $\mathcal{N}_{\leq}(a)$ of $a$ in the subspace topology on $\{x \mid x \leq a\}$ has a basis consisting of the left-open right-closed intervals $(l, a]$ for all $l < a$.

nhds_top_order theorem

 [TopologicalSpace α] [Preorder α] [OrderTop α] [OrderTopology α] : 𝓝 (⊤ : α) = ⨅ (l) (_ : l < ⊤), 𝓟 (Ioi l)

Full source

theorem nhds_top_order [TopologicalSpace α] [Preorder α] [OrderTop α] [OrderTopology α] :
    𝓝 (⊤ : α) = ⨅ (l) (_ : l < ⊤), 𝓟 (Ioi l) := by simp [nhds_eq_order (⊤ : α)]

Neighborhood Filter Characterization at Top Element in Order Topology

Informal description

Let $\alpha$ be a topological space with a preorder structure and the order topology, and assume $\alpha$ has a top element $\top$. Then the neighborhood filter of $\top$ is given by: \[ \mathcal{N}(\top) = \bigwedge_{l < \top} \mathcal{P}((l, \infty)), \] where the infimum is taken over all elements $l$ in $\alpha$ that are strictly less than $\top$.

nhds_bot_order theorem

 [TopologicalSpace α] [Preorder α] [OrderBot α] [OrderTopology α] : 𝓝 (⊥ : α) = ⨅ (l) (_ : ⊥ < l), 𝓟 (Iio l)

Full source

theorem nhds_bot_order [TopologicalSpace α] [Preorder α] [OrderBot α] [OrderTopology α] :
    𝓝 (⊥ : α) = ⨅ (l) (_ : ⊥ < l), 𝓟 (Iio l) := by simp [nhds_eq_order (⊥ : α)]

Neighborhood Filter Characterization at Bottom Element in Order Topology

Informal description

Let $\alpha$ be a topological space with a preorder structure and the order topology, and assume $\alpha$ has a bottom element $\bot$. Then the neighborhood filter of $\bot$ is given by: \[ \mathcal{N}(\bot) = \bigwedge_{l > \bot} \mathcal{P}((-\infty, l)), \] where the infimum is taken over all elements $l$ in $\alpha$ that are strictly greater than $\bot$.

nhds_top_basis theorem

 [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α] [Nontrivial α] :
  (𝓝 ⊤).HasBasis (fun a : α => a < ⊤) fun a : α => Ioi a

Full source

theorem nhds_top_basis [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α]
    [Nontrivial α] : (𝓝 ⊤).HasBasis (fun a : α => a < ⊤) fun a : α => Ioi a := by
  have : ∃ x : α, x < ⊤ := (exists_ne ⊤).imp fun x hx => hx.lt_top
  simpa only [Iic_top, nhdsWithin_univ, Ioc_top] using nhdsLE_basis_of_exists_lt this

Basis of Neighborhoods at Top Element in Order Topology: $\mathcal{N}(\top) = \{(a, \infty) \mid a < \top\}$

Informal description

Let $\alpha$ be a nontrivial linear order with a top element $\top$, equipped with the order topology. Then the neighborhood filter of $\top$ has a basis consisting of all right-infinite open intervals $(a, \infty)$ where $a$ ranges over elements of $\alpha$ strictly less than $\top$.

nhds_bot_basis theorem

 [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α] [Nontrivial α] :
  (𝓝 ⊥).HasBasis (fun a : α => ⊥ < a) fun a : α => Iio a

Full source

theorem nhds_bot_basis [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α]
    [Nontrivial α] : (𝓝 ⊥).HasBasis (fun a : α => ⊥ < a) fun a : α => Iio a :=
  nhds_top_basis (α := αᵒᵈ)

Basis of Neighborhoods at Bottom Element in Order Topology: $\mathcal{N}(\bot) = \{(-\infty, a) \mid a > \bot\}$

Informal description

Let $\alpha$ be a nontrivial linear order with a bottom element $\bot$, equipped with the order topology. Then the neighborhood filter of $\bot$ has a basis consisting of all left-infinite open intervals $(-\infty, a)$ where $a$ ranges over elements of $\alpha$ strictly greater than $\bot$.

nhds_top_basis_Ici theorem

 [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α] [Nontrivial α] [DenselyOrdered α] :
  (𝓝 ⊤).HasBasis (fun a : α => a < ⊤) Ici

Full source

theorem nhds_top_basis_Ici [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α]
    [Nontrivial α] [DenselyOrdered α] : (𝓝 ⊤).HasBasis (fun a : α => a < ⊤) Ici :=
  nhds_top_basis.to_hasBasis
    (fun _a ha => let ⟨b, hab, hb⟩ := exists_between ha; ⟨b, hb, Ici_subset_Ioi.mpr hab⟩)
    fun a ha => ⟨a, ha, Ioi_subset_Ici_self⟩

Basis of Neighborhoods at Top Element Using Closed Intervals: $\mathcal{N}(\top) = \{[a, \infty) \mid a < \top\}$

Informal description

Let $\alpha$ be a nontrivial densely ordered linear order with a top element $\top$, equipped with the order topology. Then the neighborhood filter of $\top$ has a basis consisting of all left-closed right-infinite intervals $[a, \infty)$ where $a$ ranges over elements of $\alpha$ strictly less than $\top$.

nhds_bot_basis_Iic theorem

 [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α] [Nontrivial α] [DenselyOrdered α] :
  (𝓝 ⊥).HasBasis (fun a : α => ⊥ < a) Iic

Full source

theorem nhds_bot_basis_Iic [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α]
    [Nontrivial α] [DenselyOrdered α] : (𝓝 ⊥).HasBasis (fun a : α => ⊥ < a) Iic :=
  nhds_top_basis_Ici (α := αᵒᵈ)

Basis of Neighborhoods at Bottom Element Using Closed Intervals: $\mathcal{N}(\bot) = \{(-\infty, a] \mid a > \bot\}$

Informal description

Let $\alpha$ be a nontrivial densely ordered linear order with a bottom element $\bot$, equipped with the order topology. Then the neighborhood filter of $\bot$ has a basis consisting of all left-infinite right-closed intervals $(-\infty, a]$ where $a$ ranges over elements of $\alpha$ strictly greater than $\bot$.

tendsto_nhds_top_mono theorem

 [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β] {l : Filter α} {f g : α → β} (hf : Tendsto f l (𝓝 ⊤))
  (hg : f ≤ᶠ[l] g) : Tendsto g l (𝓝 ⊤)

Full source

theorem tendsto_nhds_top_mono [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β]
    {l : Filter α} {f g : α → β} (hf : Tendsto f l (𝓝 ⊤)) (hg : f ≤ᶠ[l] g) : Tendsto g l (𝓝 ⊤) := by
  simp only [nhds_top_order, tendsto_iInf, tendsto_principal] at hf ⊢
  intro x hx
  filter_upwards [hf x hx, hg] with _ using lt_of_lt_of_le

Monotonicity of Tendency to Top in Order Topology

Informal description

Let $\beta$ be a topological space with a preorder and a greatest element $\top$, equipped with the order topology. Let $l$ be a filter on a type $\alpha$, and let $f, g : \alpha \to \beta$ be functions. If $f$ tends to $\top$ along $l$ and $f \leq g$ eventually along $l$, then $g$ also tends to $\top$ along $l$.

tendsto_nhds_bot_mono theorem

 [TopologicalSpace β] [Preorder β] [OrderBot β] [OrderTopology β] {l : Filter α} {f g : α → β} (hf : Tendsto f l (𝓝 ⊥))
  (hg : g ≤ᶠ[l] f) : Tendsto g l (𝓝 ⊥)

Full source

theorem tendsto_nhds_bot_mono [TopologicalSpace β] [Preorder β] [OrderBot β] [OrderTopology β]
    {l : Filter α} {f g : α → β} (hf : Tendsto f l (𝓝 ⊥)) (hg : g ≤ᶠ[l] f) : Tendsto g l (𝓝 ⊥) :=
  tendsto_nhds_top_mono (β := βᵒᵈ) hf hg

Monotonicity of Tendency to Bottom in Order Topology

Informal description

Let $\beta$ be a topological space with a preorder and a least element $\bot$, equipped with the order topology. Let $l$ be a filter on a type $\alpha$, and let $f, g : \alpha \to \beta$ be functions. If $f$ tends to $\bot$ along $l$ and $g \leq f$ eventually along $l$, then $g$ also tends to $\bot$ along $l$.

tendsto_nhds_top_mono' theorem

 [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β] {l : Filter α} {f g : α → β} (hf : Tendsto f l (𝓝 ⊤))
  (hg : f ≤ g) : Tendsto g l (𝓝 ⊤)

Full source

theorem tendsto_nhds_top_mono' [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β]
    {l : Filter α} {f g : α → β} (hf : Tendsto f l (𝓝 ⊤)) (hg : f ≤ g) : Tendsto g l (𝓝 ⊤) :=
  tendsto_nhds_top_mono hf (Eventually.of_forall hg)

Monotonicity of Tendency to Top in Order Topology (Pointwise Inequality)

Informal description

Let $\beta$ be a topological space with a preorder and a greatest element $\top$, equipped with the order topology. Let $l$ be a filter on a type $\alpha$, and let $f, g : \alpha \to \beta$ be functions. If $f$ tends to $\top$ along $l$ and $f(x) \leq g(x)$ for all $x \in \alpha$, then $g$ also tends to $\top$ along $l$.

tendsto_nhds_bot_mono' theorem

 [TopologicalSpace β] [Preorder β] [OrderBot β] [OrderTopology β] {l : Filter α} {f g : α → β} (hf : Tendsto f l (𝓝 ⊥))
  (hg : g ≤ f) : Tendsto g l (𝓝 ⊥)

Full source

theorem tendsto_nhds_bot_mono' [TopologicalSpace β] [Preorder β] [OrderBot β] [OrderTopology β]
    {l : Filter α} {f g : α → β} (hf : Tendsto f l (𝓝 ⊥)) (hg : g ≤ f) : Tendsto g l (𝓝 ⊥) :=
  tendsto_nhds_bot_mono hf (Eventually.of_forall hg)

Monotonicity of Tendency to Bottom in Order Topology (Pointwise Inequality)

Informal description

Let $\beta$ be a topological space with a preorder and a least element $\bot$, equipped with the order topology. Let $l$ be a filter on a type $\alpha$, and let $f, g : \alpha \to \beta$ be functions. If $f$ tends to $\bot$ along $l$ and $g(x) \leq f(x)$ for all $x \in \alpha$, then $g$ also tends to $\bot$ along $l$.

order_separated theorem

 [OrderTopology α] {a₁ a₂ : α} (h : a₁ < a₂) :
  ∃ u v : Set α, IsOpen u ∧ IsOpen v ∧ a₁ ∈ u ∧ a₂ ∈ v ∧ ∀ b₁ ∈ u, ∀ b₂ ∈ v, b₁ < b₂

Full source

theorem order_separated [OrderTopology α] {a₁ a₂ : α} (h : a₁ < a₂) :
    ∃ u v : Set α, IsOpen u ∧ IsOpen v ∧ a₁ ∈ u ∧ a₂ ∈ v ∧ ∀ b₁ ∈ u, ∀ b₂ ∈ v, b₁ < b₂ :=
  let ⟨x, hx, y, hy, h⟩ := h.exists_disjoint_Iio_Ioi
  ⟨Iio x, Ioi y, isOpen_gt' _, isOpen_lt' _, hx, hy, h⟩

Separation of Points in Order Topology by Open Sets

Informal description

Let $\alpha$ be a topological space with an order topology and $a_1, a_2 \in \alpha$ such that $a_1 < a_2$. Then there exist open sets $U$ and $V$ in $\alpha$ such that: - $U$ and $V$ are open, - $a_1 \in U$ and $a_2 \in V$, - For all $b_1 \in U$ and $b_2 \in V$, we have $b_1 < b_2$.

OrderTopology.to_orderClosedTopology instance

[OrderTopology α] : OrderClosedTopology α

Full source

instance (priority := 100) OrderTopology.to_orderClosedTopology [OrderTopology α] :
    OrderClosedTopology α where
  isClosed_le' := isOpen_compl_iff.1 <| isOpen_prod_iff.mpr fun a₁ a₂ (h : ¬a₁ ≤ a₂) =>
    have h : a₂ < a₁ := lt_of_not_ge h
    let ⟨u, v, hu, hv, ha₁, ha₂, h⟩ := order_separated h
    ⟨v, u, hv, hu, ha₂, ha₁, fun ⟨b₁, b₂⟩ ⟨h₁, h₂⟩ => not_le_of_gt <| h b₂ h₂ b₁ h₁⟩

Order Topology Implies Order-Closed Topology

Informal description

For any topological space $\alpha$ with a preorder structure, if the topology on $\alpha$ coincides with the order topology (i.e., it is generated by open intervals), then $\alpha$ is an order-closed topological space. This means that the set $\{(x, y) \in \alpha \times \alpha \mid x \leq y\}$ is closed in the product topology.

exists_Ioc_subset_of_mem_nhds theorem

[OrderTopology α] {a : α} {s : Set α} (hs : s ∈ 𝓝 a) (h : ∃ l, l < a) : ∃ l < a, Ioc l a ⊆ s

Full source

theorem exists_Ioc_subset_of_mem_nhds [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ 𝓝 a)
    (h : ∃ l, l < a) : ∃ l < a, Ioc l a ⊆ s :=
  (nhdsLE_basis_of_exists_lt h).mem_iff.mp (nhdsWithin_le_nhds hs)

Existence of Ioc Subset in Neighborhood for Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a \in \alpha$ be a point such that there exists some $l < a$. For any neighborhood $s$ of $a$, there exists an element $l < a$ such that the left-open right-closed interval $(l, a]$ is contained in $s$.

exists_Ioc_subset_of_mem_nhds' theorem

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

Full source

theorem exists_Ioc_subset_of_mem_nhds' [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ 𝓝 a) {l : α}
    (hl : l < a) : ∃ l' ∈ Ico l a, Ioc l' a ⊆ s :=
  let ⟨l', hl'a, hl's⟩ := exists_Ioc_subset_of_mem_nhds hs ⟨l, hl⟩
  ⟨max l l', ⟨le_max_left _ _, max_lt hl hl'a⟩,
    (Ioc_subset_Ioc_left <| le_max_right _ _).trans hl's⟩

Existence of Refined Ioc Subset in Neighborhood for Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a \in \alpha$ be a point. Given a neighborhood $s$ of $a$ and an element $l < a$, there exists an element $l'$ in the interval $[l, a)$ such that the left-open right-closed interval $(l', a]$ is contained in $s$.

exists_Ico_subset_of_mem_nhds' theorem

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

Full source

theorem exists_Ico_subset_of_mem_nhds' [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ 𝓝 a) {u : α}
    (hu : a < u) : ∃ u' ∈ Ioc a u, Ico a u' ⊆ s := by
  simpa only [OrderDual.exists, exists_prop, Ico_toDual, Ioc_toDual] using
    exists_Ioc_subset_of_mem_nhds' (show ofDualofDual ⁻¹' sofDual ⁻¹' s ∈ 𝓝 (toDual a) from hs) hu.dual

Existence of Refined Ico Subset in Neighborhood for Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a \in \alpha$ be a point. Given a neighborhood $s$ of $a$ and an element $u > a$, there exists an element $u'$ in the interval $(a, u]$ such that the left-closed right-open interval $[a, u')$ is contained in $s$.

exists_Ico_subset_of_mem_nhds theorem

[OrderTopology α] {a : α} {s : Set α} (hs : s ∈ 𝓝 a) (h : ∃ u, a < u) : ∃ u, a < u ∧ Ico a u ⊆ s

Full source

theorem exists_Ico_subset_of_mem_nhds [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ 𝓝 a)
    (h : ∃ u, a < u) : ∃ u, a < u ∧ Ico a u ⊆ s :=
  let ⟨_l', hl'⟩ := h
  let ⟨l, hl⟩ := exists_Ico_subset_of_mem_nhds' hs hl'
  ⟨l, hl.1.1, hl.2⟩

Existence of Right Neighborhood Interval in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a \in \alpha$ be a point. Given a neighborhood $s$ of $a$ and the existence of an element $u > a$, there exists an element $u > a$ such that the left-closed right-open interval $[a, u)$ is contained in $s$.

exists_Icc_mem_subset_of_mem_nhdsGE theorem

 [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ 𝓝[≥] a) : ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Full source

theorem exists_Icc_mem_subset_of_mem_nhdsGE [OrderTopology α] {a : α} {s : Set α}
    (hs : s ∈ 𝓝[≥] a) : ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s := by
  rcases (em (IsMax a)).imp_right not_isMax_iff.mp with (ha | ha)
  · use a
    simpa [ha.Ici_eq] using hs
  · rcases(nhdsGE_basis_of_exists_gt ha).mem_iff.mp hs with ⟨b, hab, hbs⟩
    rcases eq_empty_or_nonempty (Ioo a b) with (H | ⟨c, hac, hcb⟩)
    · have : Ico a b = Icc a a := by rw [← Icc_union_Ioo_eq_Ico le_rfl hab, H, union_empty]
      exact ⟨a, le_rfl, this ▸ ⟨Ico_mem_nhdsGE hab, hbs⟩⟩
    · refine ⟨c, hac.le, Icc_mem_nhdsGE hac, ?_⟩
      exact (Icc_subset_Ico_right hcb).trans hbs

Existence of Closed Interval Neighborhood in Right-Neighborhood Filter for Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a \in \alpha$. For any neighborhood $s$ of $a$ in the right-neighborhood filter $\mathcal{N}_{\geq a}$, there exists an element $b \geq a$ such that the closed interval $[a, b]$ is both a neighborhood of $a$ in $\mathcal{N}_{\geq a}$ and a subset of $s$.

exists_Icc_mem_subset_of_mem_nhdsLE theorem

 [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ 𝓝[≤] a) : ∃ b ≤ a, Icc b a ∈ 𝓝[≤] a ∧ Icc b a ⊆ s

Full source

theorem exists_Icc_mem_subset_of_mem_nhdsLE [OrderTopology α] {a : α} {s : Set α}
    (hs : s ∈ 𝓝[≤] a) : ∃ b ≤ a, Icc b a ∈ 𝓝[≤] a ∧ Icc b a ⊆ s := by
  simpa only [Icc_toDual, toDual.surjective.exists] using
    exists_Icc_mem_subset_of_mem_nhdsGE (α := αᵒᵈ) (a := toDual a) hs

Existence of Closed Interval Neighborhood in Left-Neighborhood Filter for Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a \in \alpha$. For any neighborhood $s$ of $a$ in the left-neighborhood filter $\mathcal{N}_{\leq a}$, there exists an element $b \leq a$ such that the closed interval $[b, a]$ is both a neighborhood of $a$ in $\mathcal{N}_{\leq a}$ and a subset of $s$.

exists_Icc_mem_subset_of_mem_nhds theorem

 [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ 𝓝 a) : ∃ b c, a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s

Full source

theorem exists_Icc_mem_subset_of_mem_nhds [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ 𝓝 a) :
    ∃ b c, a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s := by
  rcases exists_Icc_mem_subset_of_mem_nhdsLE (nhdsWithin_le_nhds hs) with
    ⟨b, hba, hb_nhds, hbs⟩
  rcases exists_Icc_mem_subset_of_mem_nhdsGE (nhdsWithin_le_nhds hs) with
    ⟨c, hac, hc_nhds, hcs⟩
  refine ⟨b, c, ⟨hba, hac⟩, ?_⟩
  rw [← Icc_union_Icc_eq_Icc hba hac, ← nhdsLE_sup_nhdsGE]
  exact ⟨union_mem_sup hb_nhds hc_nhds, union_subset hbs hcs⟩

Existence of Closed Interval Neighborhood in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a \in \alpha$. For any neighborhood $s$ of $a$ in the neighborhood filter $\mathcal{N}(a)$, there exist elements $b, c \in \alpha$ such that $a \in [b, c]$, the closed interval $[b, c]$ is a neighborhood of $a$, and $[b, c] \subseteq s$.

IsOpen.exists_Ioo_subset theorem

[OrderTopology α] [Nontrivial α] {s : Set α} (hs : IsOpen s) (h : s.Nonempty) : ∃ a b, a < b ∧ Ioo a b ⊆ s

Full source

theorem IsOpen.exists_Ioo_subset [OrderTopology α] [Nontrivial α] {s : Set α} (hs : IsOpen s)
    (h : s.Nonempty) : ∃ a b, a < b ∧ Ioo a b ⊆ s := by
  obtain ⟨x, hx⟩ : ∃ x, x ∈ s := h
  obtain ⟨y, hy⟩ : ∃ y, y ≠ x := exists_ne x
  rcases lt_trichotomy x y with (H | rfl | H)
  · obtain ⟨u, xu, hu⟩ : ∃ u, x < u ∧ Ico x u ⊆ s :=
      exists_Ico_subset_of_mem_nhds (hs.mem_nhds hx) ⟨y, H⟩
    exact ⟨x, u, xu, Ioo_subset_Ico_self.trans hu⟩
  · exact (hy rfl).elim
  · obtain ⟨l, lx, hl⟩ : ∃ l, l < x ∧ Ioc l x ⊆ s :=
      exists_Ioc_subset_of_mem_nhds (hs.mem_nhds hx) ⟨y, H⟩
    exact ⟨l, x, lx, Ioo_subset_Ioc_self.trans hl⟩

Existence of Open Interval in Nonempty Open Set for Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology and assume $\alpha$ is nontrivial. For any nonempty open set $s \subseteq \alpha$, there exist elements $a, b \in \alpha$ with $a < b$ such that the open interval $(a, b)$ is contained in $s$.

dense_of_exists_between theorem

[OrderTopology α] [Nontrivial α] {s : Set α} (h : ∀ ⦃a b⦄, a < b → ∃ c ∈ s, a < c ∧ c < b) : Dense s

Full source

theorem dense_of_exists_between [OrderTopology α] [Nontrivial α] {s : Set α}
    (h : ∀ ⦃a b⦄, a < b → ∃ c ∈ s, a < c ∧ c < b) : Dense s := by
  refine dense_iff_inter_open.2 fun U U_open U_nonempty => ?_
  obtain ⟨a, b, hab, H⟩ : ∃ a b : α, a < b ∧ Ioo a b ⊆ U := U_open.exists_Ioo_subset U_nonempty
  obtain ⟨x, xs, hx⟩ : ∃ x ∈ s, a < x ∧ x < b := h hab
  exact ⟨x, ⟨H hx, xs⟩⟩

Density via Betweenness in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology and assume $\alpha$ is nontrivial. For a subset $s \subseteq \alpha$, if for any two elements $a, b \in \alpha$ with $a < b$ there exists an element $c \in s$ such that $a < c < b$, then $s$ is dense in $\alpha$.

dense_iff_exists_between theorem

 [OrderTopology α] [DenselyOrdered α] [Nontrivial α] {s : Set α} : Dense s ↔ ∀ a b, a < b → ∃ c ∈ s, a < c ∧ c < b

Full source

/-- A set in a nontrivial densely linear ordered type is dense in the sense of topology if and only
if for any `a < b` there exists `c ∈ s`, `a < c < b`. Each implication requires less typeclass
assumptions. -/
theorem dense_iff_exists_between [OrderTopology α] [DenselyOrdered α] [Nontrivial α] {s : Set α} :
    DenseDense s ↔ ∀ a b, a < b → ∃ c ∈ s, a < c ∧ c < b :=
  ⟨fun h _ _ hab => h.exists_between hab, dense_of_exists_between⟩

Density Characterization via Betweenness in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology, densely ordered, and nontrivial. A subset $s \subseteq \alpha$ is dense if and only if for any two elements $a, b \in \alpha$ with $a < b$, there exists an element $c \in s$ such that $a < c < b$.

mem_nhds_iff_exists_Ioo_subset' theorem

 [OrderTopology α] {a : α} {s : Set α} (hl : ∃ l, l < a) (hu : ∃ u, a < u) : s ∈ 𝓝 a ↔ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

Full source

/-- A set is a neighborhood of `a` if and only if it contains an interval `(l, u)` containing `a`,
provided `a` is neither a bottom element nor a top element. -/
theorem mem_nhds_iff_exists_Ioo_subset' [OrderTopology α] {a : α} {s : Set α} (hl : ∃ l, l < a)
    (hu : ∃ u, a < u) : s ∈ 𝓝 as ∈ 𝓝 a ↔ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s := by
  constructor
  · intro h
    rcases exists_Ico_subset_of_mem_nhds h hu with ⟨u, au, hu⟩
    rcases exists_Ioc_subset_of_mem_nhds h hl with ⟨l, la, hl⟩
    exact ⟨l, u, ⟨la, au⟩, Ioc_union_Ico_eq_Ioo la au ▸ union_subset hl hu⟩
  · rintro ⟨l, u, ha, h⟩
    apply mem_of_superset (Ioo_mem_nhds ha.1 ha.2) h

Neighborhood Characterization via Open Intervals in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a \in \alpha$ be a point such that there exist elements $l < a$ and $u > a$. A set $s$ is a neighborhood of $a$ if and only if there exist elements $l$ and $u$ such that $a \in (l, u)$ and the open interval $(l, u)$ is contained in $s$.

mem_nhds_iff_exists_Ioo_subset theorem

 [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] {a : α} {s : Set α} : s ∈ 𝓝 a ↔ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

Full source

/-- A set is a neighborhood of `a` if and only if it contains an interval `(l, u)` containing `a`.
-/
theorem mem_nhds_iff_exists_Ioo_subset [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] {a : α}
    {s : Set α} : s ∈ 𝓝 as ∈ 𝓝 a ↔ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s :=
  mem_nhds_iff_exists_Ioo_subset' (exists_lt a) (exists_gt a)

Neighborhood Characterization via Open Intervals in Order Topology without Extrema

Informal description

Let $\alpha$ be a topological space with an order topology, where $\alpha$ has no maximal or minimal elements. For any point $a \in \alpha$ and any set $s \subseteq \alpha$, the set $s$ is a neighborhood of $a$ if and only if there exist elements $l, u \in \alpha$ such that $a \in (l, u)$ and the open interval $(l, u)$ is contained in $s$.

nhds_basis_Ioo' theorem

 [OrderTopology α] {a : α} (hl : ∃ l, l < a) (hu : ∃ u, a < u) :
  (𝓝 a).HasBasis (fun b : α × α => b.1 < a ∧ a < b.2) fun b => Ioo b.1 b.2

Full source

theorem nhds_basis_Ioo' [OrderTopology α] {a : α} (hl : ∃ l, l < a) (hu : ∃ u, a < u) :
    (𝓝 a).HasBasis (fun b : α × α => b.1 < a ∧ a < b.2) fun b => Ioo b.1 b.2 :=
  ⟨fun s => (mem_nhds_iff_exists_Ioo_subset' hl hu).trans <| by simp⟩

Basis of Neighborhoods in Order Topology via Open Intervals

Informal description

Let $\alpha$ be a topological space with an order topology, and let $a \in \alpha$ be a point such that there exist elements $l < a$ and $u > a$. The neighborhood filter $\mathcal{N}(a)$ has a basis consisting of open intervals $(l, u)$ where $l < a < u$.

nhds_basis_Ioo theorem

 [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] (a : α) :
  (𝓝 a).HasBasis (fun b : α × α => b.1 < a ∧ a < b.2) fun b => Ioo b.1 b.2

Full source

theorem nhds_basis_Ioo [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] (a : α) :
    (𝓝 a).HasBasis (fun b : α × α => b.1 < a ∧ a < b.2) fun b => Ioo b.1 b.2 :=
  nhds_basis_Ioo' (exists_lt a) (exists_gt a)

Basis of Neighborhoods via Open Intervals in Order Topology without Extrema

Informal description

Let $\alpha$ be a topological space with an order topology and no maximal or minimal elements. For any point $a \in \alpha$, the neighborhood filter $\mathcal{N}(a)$ has a basis consisting of open intervals $(l, u)$ where $l < a < u$.

Filter.Eventually.exists_Ioo_subset theorem

 [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] {a : α} {p : α → Prop} (hp : ∀ᶠ x in 𝓝 a, p x) :
  ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ {x | p x}

Full source

theorem Filter.Eventually.exists_Ioo_subset [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] {a : α}
    {p : α → Prop} (hp : ∀ᶠ x in 𝓝 a, p x) : ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ { x | p x } :=
  mem_nhds_iff_exists_Ioo_subset.1 hp

Existence of Open Interval Subset in Neighborhood for Order Topology without Extrema

Informal description

Let $\alpha$ be a topological space with an order topology, where $\alpha$ has no maximal or minimal elements. For any point $a \in \alpha$ and any property $p$ on $\alpha$, if $p(x)$ holds for all $x$ in some neighborhood of $a$, then there exist elements $l, u \in \alpha$ such that $a \in (l, u)$ and the property $p$ holds for all $x \in (l, u)$.

Dense.topology_eq_generateFrom theorem

 [OrderTopology α] [DenselyOrdered α] {s : Set α} (hs : Dense s) :
  ‹TopologicalSpace α› = .generateFrom (Ioi '' s ∪ Iio '' s)

Full source

theorem Dense.topology_eq_generateFrom [OrderTopology α] [DenselyOrdered α] {s : Set α}
    (hs : Dense s) : ‹TopologicalSpace α› = .generateFrom (IoiIoi '' sIoi '' s ∪ Iio '' s) := by
  refine (OrderTopology.topology_eq_generate_intervals (α := α)).trans ?_
  refine le_antisymm (generateFrom_anti ?_) (le_generateFrom ?_)
  · simp only [union_subset_iff, image_subset_iff]
    exact ⟨fun a _ ↦ ⟨a, .inl rfl⟩, fun a _ ↦ ⟨a, .inr rfl⟩⟩
  · rintro _ ⟨a, rfl | rfl⟩
    · rw [hs.Ioi_eq_biUnion]
      let _ := generateFrom (IoiIoi '' sIoi '' s ∪ Iio '' s)
      exact isOpen_iUnion fun x ↦ isOpen_iUnion fun h ↦ .basic _ <| .inl <| mem_image_of_mem _ h.1
    · rw [hs.Iio_eq_biUnion]
      let _ := generateFrom (IoiIoi '' sIoi '' s ∪ Iio '' s)
      exact isOpen_iUnion fun x ↦ isOpen_iUnion fun h ↦ .basic _ <| .inr <| mem_image_of_mem _ h.1

Order Topology Generated by Dense Subset Intervals

Informal description

Let $\alpha$ be a topological space with an order topology and a dense order, and let $s$ be a dense subset of $\alpha$. Then the topology on $\alpha$ is equal to the topology generated by the union of all right-infinite open intervals $(a, \infty)$ with $a \in s$ and all left-infinite open intervals $(-\infty, b)$ with $b \in s$. In other words: $$\text{Topology on } \alpha = \text{Topology generated by } \{(a, \infty) \mid a \in s\} \cup \{(-\infty, b) \mid b \in s\}.$$

PredOrder.hasBasis_nhds_Ioc_of_exists_gt theorem

[OrderTopology α] [PredOrder α] {a : α} (ha : ∃ u, a < u) : (𝓝 a).HasBasis (a < ·) (Set.Ico a ·)

Full source

theorem PredOrder.hasBasis_nhds_Ioc_of_exists_gt [OrderTopology α] [PredOrder α] {a : α}
    (ha : ∃ u, a < u) : (𝓝 a).HasBasis (a < ·) (Set.Ico a ·) :=
  PredOrder.nhdsGE_eq_nhds a ▸ nhdsGE_basis_of_exists_gt ha

Basis Characterization of Neighborhood Filter via $[a, u)$ Intervals in PredOrder Topology

Informal description

Let $\alpha$ be a topological space with a linear order and the order topology, equipped with a predecessor order structure (`PredOrder`). For any element $a \in \alpha$ such that there exists $u$ with $a < u$, the neighborhood filter $\mathcal{N}(a)$ of $a$ has a basis consisting of the left-closed right-open intervals $[a, u)$ for all $u > a$. In other words, the filter $\mathcal{N}(a)$ is generated by the sets $[a, u)$ where $u$ ranges over all elements greater than $a$.

PredOrder.hasBasis_nhds_Ioc theorem

[OrderTopology α] [PredOrder α] [NoMaxOrder α] {a : α} : (𝓝 a).HasBasis (a < ·) (Set.Ico a ·)

Full source

theorem PredOrder.hasBasis_nhds_Ioc [OrderTopology α] [PredOrder α] [NoMaxOrder α] {a : α} :
    (𝓝 a).HasBasis (a < ·) (Set.Ico a ·) :=
  PredOrder.hasBasis_nhds_Ioc_of_exists_gt (exists_gt a)

Neighborhood Basis via $[a, u)$ Intervals in PredOrder Topology Without Maximal Element

Informal description

Let $\alpha$ be a topological space with an order topology and a predecessor order structure (`PredOrder`), and assume $\alpha$ has no maximal element. Then for any element $a \in \alpha$, the neighborhood filter $\mathcal{N}(a)$ of $a$ has a basis consisting of the left-closed right-open intervals $[a, u)$ for all $u > a$. In other words, the filter $\mathcal{N}(a)$ is generated by the sets $\{x \in \alpha \mid a \leq x < u\}$ where $u$ ranges over all elements greater than $a$.

SuccOrder.hasBasis_nhds_Ioc_of_exists_lt theorem

[OrderTopology α] [SuccOrder α] {a : α} (ha : ∃ l, l < a) : (𝓝 a).HasBasis (· < a) (Set.Ioc · a)

Full source

theorem SuccOrder.hasBasis_nhds_Ioc_of_exists_lt [OrderTopology α] [SuccOrder α] {a : α}
    (ha : ∃ l, l < a) : (𝓝 a).HasBasis (· < a) (Set.Ioc · a) :=
  SuccOrder.nhdsLE_eq_nhds a ▸ nhdsLE_basis_of_exists_lt ha

Basis Characterization of Neighborhood Filter via $(l, a]$ Intervals in SuccOrder Topology

Informal description

Let $\alpha$ be a topological space with a linear order and the order topology, equipped with a successor order structure (`SuccOrder`). For any element $a \in \alpha$ such that there exists $l$ with $l < a$, the neighborhood filter $\mathcal{N}(a)$ of $a$ has a basis consisting of the left-open right-closed intervals $(l, a]$ for all $l < a$. In other words, the filter $\mathcal{N}(a)$ is generated by the sets $(l, a]$ where $l$ ranges over all elements less than $a$.

SuccOrder.hasBasis_nhds_Ioc theorem

[OrderTopology α] [SuccOrder α] {a : α} [NoMinOrder α] : (𝓝 a).HasBasis (· < a) (Set.Ioc · a)

Full source

theorem SuccOrder.hasBasis_nhds_Ioc [OrderTopology α] [SuccOrder α] {a : α} [NoMinOrder α] :
    (𝓝 a).HasBasis (· < a) (Set.Ioc · a) :=
  SuccOrder.hasBasis_nhds_Ioc_of_exists_lt (exists_lt a)

Neighborhood Basis via $(l, a]$ Intervals in SuccOrder Topology Without Minimal Element

Informal description

Let $\alpha$ be a topological space with an order topology and a successor order structure (`SuccOrder`), and assume $\alpha$ has no minimal element. Then for any element $a \in \alpha$, the neighborhood filter $\mathcal{N}(a)$ of $a$ has a basis consisting of the left-open right-closed intervals $(l, a]$ for all $l < a$. In other words, the filter $\mathcal{N}(a)$ is generated by the sets $\{x \in \alpha \mid l < x \leq a\}$ where $l$ ranges over all elements less than $a$.

SecondCountableTopology.of_separableSpace_orderTopology theorem

[OrderTopology α] [DenselyOrdered α] [SeparableSpace α] : SecondCountableTopology α

Full source

/-- Let `α` be a densely ordered linear order with order topology. If `α` is a separable space, then
it has second countable topology. Note that the "densely ordered" assumption cannot be dropped, see
[double arrow space](https://topology.pi-base.org/spaces/S000093) for a counterexample. -/
theorem SecondCountableTopology.of_separableSpace_orderTopology [OrderTopology α] [DenselyOrdered α]
    [SeparableSpace α] : SecondCountableTopology α := by
  rcases exists_countable_dense α with ⟨s, hc, hd⟩
  refine ⟨⟨_, ?_, hd.topology_eq_generateFrom⟩⟩
  exact (hc.image _).union (hc.image _)

Second Countability of Separable Densely Ordered Spaces with Order Topology

Informal description

Let $\alpha$ be a densely ordered linear order with the order topology. If $\alpha$ is a separable space, then the topology on $\alpha$ is second countable.

countable_setOf_covBy_right theorem

[OrderTopology α] [SecondCountableTopology α] : Set.Countable {x : α | ∃ y, x ⋖ y}

Full source

/-- The set of points which are isolated on the right is countable when the space is
second-countable. -/
theorem countable_setOf_covBy_right [OrderTopology α] [SecondCountableTopology α] :
    Set.Countable { x : α | ∃ y, x ⋖ y } := by
  nontriviality α
  let s := { x : α | ∃ y, x ⋖ y }
  have : ∀ x ∈ s, ∃ y, x ⋖ y := fun x => id
  choose! y hy using this
  have Hy : ∀ x z, x ∈ s → z < y x → z ≤ x := fun x z hx => (hy x hx).le_of_lt
  suffices H : ∀ a : Set α, IsOpen a → Set.Countable { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a } by
    have : s ⊆ ⋃ a ∈ countableBasis α, { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a } := fun x hx => by
      rcases (isBasis_countableBasis α).exists_mem_of_ne (hy x hx).ne with ⟨a, ab, xa, ya⟩
      exact mem_iUnion₂.2 ⟨a, ab, hx, xa, ya⟩
    refine Set.Countable.mono this ?_
    refine Countable.biUnion (countable_countableBasis α) fun a ha => H _ ?_
    exact isOpen_of_mem_countableBasis ha
  intro a ha
  suffices H : Set.Countable { x | (x ∈ s ∧ x ∈ a ∧ y x ∉ a) ∧ ¬IsBot x } from
    H.of_diff (subsingleton_isBot α).countable
  simp only [and_assoc]
  let t := { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x }
  have : ∀ x ∈ t, ∃ z < x, Ioc z x ⊆ a := by
    intro x hx
    apply exists_Ioc_subset_of_mem_nhds (ha.mem_nhds hx.2.1)
    simpa only [IsBot, not_forall, not_le] using hx.right.right.right
  choose! z hz h'z using this
  have : PairwiseDisjoint t fun x => Ioc (z x) x := fun x xt x' x't hxx' => by
    rcases hxx'.lt_or_lt with (h' | h')
    · refine disjoint_left.2 fun u ux ux' => xt.2.2.1 ?_
      refine h'z x' x't ⟨ux'.1.trans_le (ux.2.trans (hy x xt.1).le), ?_⟩
      by_contra! H
      exact lt_irrefl _ ((Hy _ _ xt.1 H).trans_lt h')
    · refine disjoint_left.2 fun u ux ux' => x't.2.2.1 ?_
      refine h'z x xt ⟨ux.1.trans_le (ux'.2.trans (hy x' x't.1).le), ?_⟩
      by_contra! H
      exact lt_irrefl _ ((Hy _ _ x't.1 H).trans_lt h')
  refine this.countable_of_isOpen (fun x hx => ?_) fun x hx => ⟨x, hz x hx, le_rfl⟩
  suffices H : Ioc (z x) x = Ioo (z x) (y x) by
    rw [H]
    exact isOpen_Ioo
  exact Subset.antisymm (Ioc_subset_Ioo_right (hy x hx.1).lt) fun u hu => ⟨hu.1, Hy _ _ hx.1 hu.2⟩

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

Informal description

Let $\alpha$ be a topological space with an order topology and a second-countable topology. Then the set of points $x \in \alpha$ for which there exists a point $y$ such that $x$ is covered by $y$ (i.e., $x \lessdot y$) is countable.

countable_setOf_covBy_left theorem

[OrderTopology α] [SecondCountableTopology α] : Set.Countable {x : α | ∃ y, y ⋖ x}

Full source

/-- The set of points which are isolated on the left is countable when the space is
second-countable. -/
theorem countable_setOf_covBy_left [OrderTopology α] [SecondCountableTopology α] :
    Set.Countable { x : α | ∃ y, y ⋖ x } := by
  convert countable_setOf_covBy_right (α := αᵒᵈ) using 5
  exact toDual_covBy_toDual_iff.symm

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

Informal description

Let $\alpha$ be a topological space with an order topology and a second-countable topology. Then the set of points $x \in \alpha$ for which there exists a point $y$ such that $y$ is covered by $x$ (i.e., $y \lessdot x$) is countable.

countable_of_isolated_left' theorem

[OrderTopology α] [SecondCountableTopology α] : Set.Countable {x : α | ∃ y, y < x ∧ Ioo y x = ∅}

Full source

/-- The set of points which are isolated on the left is countable when the space is
second-countable. -/
theorem countable_of_isolated_left' [OrderTopology α] [SecondCountableTopology α] :
    Set.Countable { x : α | ∃ y, y < x ∧ Ioo y x = ∅ } := by
  simpa only [← covBy_iff_Ioo_eq] using countable_setOf_covBy_left

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

Informal description

Let $\alpha$ be a topological space with an order topology and a second-countable topology. Then the set of points $x \in \alpha$ for which there exists a point $y$ such that $y < x$ and the open interval $(y, x)$ is empty, is countable.

Set.PairwiseDisjoint.countable_of_Ioo theorem

 [OrderTopology α] [SecondCountableTopology α] {y : α → α} {s : Set α} (h : PairwiseDisjoint s fun x => Ioo x (y x))
  (h' : ∀ x ∈ s, x < y x) : s.Countable

Full source

/-- Consider a disjoint family of intervals `(x, y)` with `x < y` in a second-countable space.
Then the family is countable.
This is not a straightforward consequence of second-countability as some of these intervals might be
empty (but in fact this can happen only for countably many of them). -/
theorem Set.PairwiseDisjoint.countable_of_Ioo [OrderTopology α] [SecondCountableTopology α]
    {y : α → α} {s : Set α} (h : PairwiseDisjoint s fun x => Ioo x (y x))
    (h' : ∀ x ∈ s, x < y x) : s.Countable :=
  have : (s \ { x | ∃ y, x ⋖ y }).Countable :=
    (h.subset diff_subset).countable_of_isOpen (fun _ _ => isOpen_Ioo)
      fun x hx => (h' _ hx.1).exists_lt_lt (mt (Exists.intro (y x)) hx.2)
  this.of_diff countable_setOf_covBy_right

Countability of Points with Pairwise Disjoint Open Intervals in Second-Countable Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology and a second-countable topology. Given a set $s \subseteq \alpha$ and a function $y \colon \alpha \to \alpha$ such that for every $x \in s$, the open intervals $Ioo(x, y(x))$ are pairwise disjoint and $x < y(x)$, then the set $s$ is countable.

countable_image_lt_image_Ioi theorem

 [OrderTopology α] [LinearOrder β] (f : β → α) [SecondCountableTopology α] :
  Set.Countable {x | ∃ z, f x < z ∧ ∀ y, x < y → z ≤ f y}

Full source

/-- For a function taking values in a second countable space, the set of points `x` for
which the image under `f` of `(x, ∞)` is separated above from `f x` is countable. -/
theorem countable_image_lt_image_Ioi [OrderTopology α] [LinearOrder β] (f : β → α)
    [SecondCountableTopology α] : Set.Countable {x | ∃ z, f x < z ∧ ∀ y, x < y → z ≤ f y} := by
  /- If the values of `f` are separated above on the right of `x`, there is an interval `(f x, z x)`
    which is not reached by `f`. This gives a family of disjoint open intervals in `α`. Such a
    family can only be countable as `α` is second-countable. -/
  nontriviality β
  have : Nonempty α := Nonempty.map f (by infer_instance)
  let s := {x | ∃ z, f x < z ∧ ∀ y, x < y → z ≤ f y}
  have : ∀ x, x ∈ s → ∃ z, f x < z ∧ ∀ y, x < y → z ≤ f y := fun x hx ↦ hx
  -- choose `z x` such that `f` does not take the values in `(f x, z x)`.
  choose! z hz using this
  have I : InjOn f s := by
    apply StrictMonoOn.injOn
    intro x hx y _ hxy
    calc
      f x < z x := (hz x hx).1
      _ ≤ f y := (hz x hx).2 y hxy
  -- show that `f s` is countable by arguing that a disjoint family of disjoint open intervals
  -- (the intervals `(f x, z x)`) is at most countable.
  have fs_count : (f '' s).Countable := by
    have A : (f '' s).PairwiseDisjoint fun x => Ioo x (z (invFunOn f s x)) := by
      rintro _ ⟨u, us, rfl⟩ _ ⟨v, vs, rfl⟩ huv
      wlog hle : u ≤ v generalizing u v
      · exact (this v vs u us huv.symm (le_of_not_le hle)).symm
      have hlt : u < v := hle.lt_of_ne (ne_of_apply_ne _ huv)
      apply disjoint_iff_forall_ne.2
      rintro a ha b hb rfl
      simp only [I.leftInvOn_invFunOn us, I.leftInvOn_invFunOn vs] at ha hb
      exact lt_irrefl _ ((ha.2.trans_le ((hz u us).2 v hlt)).trans hb.1)
    apply Set.PairwiseDisjoint.countable_of_Ioo A
    rintro _ ⟨y, ys, rfl⟩
    simpa only [I.leftInvOn_invFunOn ys] using (hz y ys).1
  exact MapsTo.countable_of_injOn (mapsTo_image f s) I fs_count

Countability of Points with Upper-Bounded Images in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology and a second-countable topology, and let $\beta$ be a linearly ordered set. For any function $f \colon \beta \to \alpha$, the set of points $x \in \beta$ for which there exists $z \in \alpha$ such that $f(x) < z$ and for all $y > x$, $z \leq f(y)$, is countable.

countable_image_gt_image_Ioi theorem

 [OrderTopology α] [LinearOrder β] (f : β → α) [SecondCountableTopology α] :
  Set.Countable {x | ∃ z, z < f x ∧ ∀ y, x < y → f y ≤ z}

Full source

/-- For a function taking values in a second countable space, the set of points `x` for
which the image under `f` of `(x, ∞)` is separated below from `f x` is countable. -/
theorem countable_image_gt_image_Ioi [OrderTopology α] [LinearOrder β] (f : β → α)
    [SecondCountableTopology α] : Set.Countable {x | ∃ z, z < f x ∧ ∀ y, x < y → f y ≤ z} :=
  countable_image_lt_image_Ioi (α := αᵒᵈ) f

Countability of Points with Lower-Bounded Images in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology and a second-countable topology, and let $\beta$ be a linearly ordered set. For any function $f \colon \beta \to \alpha$, the set of points $x \in \beta$ for which there exists $z \in \alpha$ such that $z < f(x)$ and for all $y > x$, $f(y) \leq z$, is countable.

countable_image_lt_image_Iio theorem

 [OrderTopology α] [LinearOrder β] (f : β → α) [SecondCountableTopology α] :
  Set.Countable {x | ∃ z, f x < z ∧ ∀ y, y < x → z ≤ f y}

Full source

/-- For a function taking values in a second countable space, the set of points `x` for
which the image under `f` of `(-∞, x)` is separated above from `f x` is countable. -/
theorem countable_image_lt_image_Iio [OrderTopology α] [LinearOrder β] (f : β → α)
    [SecondCountableTopology α] : Set.Countable {x | ∃ z, f x < z ∧ ∀ y, y < x → z ≤ f y} :=
  countable_image_lt_image_Ioi (β := βᵒᵈ) f

Countability of Points with Lower-Bounded Images in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology and a second-countable topology, and let $\beta$ be a linearly ordered set. For any function $f \colon \beta \to \alpha$, the set of points $x \in \beta$ for which there exists $z \in \alpha$ such that $f(x) < z$ and for all $y < x$, $z \leq f(y)$, is countable.

countable_image_gt_image_Iio theorem

 [OrderTopology α] [LinearOrder β] (f : β → α) [SecondCountableTopology α] :
  Set.Countable {x | ∃ z, z < f x ∧ ∀ y, y < x → f y ≤ z}

Full source

/-- For a function taking values in a second countable space, the set of points `x` for
which the image under `f` of `(-∞, x)` is separated below from `f x` is countable. -/
theorem countable_image_gt_image_Iio [OrderTopology α] [LinearOrder β] (f : β → α)
    [SecondCountableTopology α] : Set.Countable {x | ∃ z, z < f x ∧ ∀ y, y < x → f y ≤ z} :=
  countable_image_lt_image_Ioi (α := αᵒᵈ) (β := βᵒᵈ) f

Countability of Points with Lower-Bounded Images in Order Topology

Informal description

Let $\alpha$ be a topological space with an order topology and a second-countable topology, and let $\beta$ be a linearly ordered set. For any function $f \colon \beta \to \alpha$, the set of points $x \in \beta$ for which there exists $z \in \alpha$ such that $z < f(x)$ and for all $y < x$, $f(y) \leq z$, is countable.

instIsCountablyGenerated_atTop instance

[OrderTopology α] [SecondCountableTopology α] : IsCountablyGenerated (atTop : Filter α)

Full source

instance instIsCountablyGenerated_atTop [OrderTopology α] [SecondCountableTopology α] :
    IsCountablyGenerated (atTop : Filter α) := by
  by_cases h : ∃ (x : α), IsTop x
  · rcases h with ⟨x, hx⟩
    rw [atTop_eq_pure_of_isTop hx]
    exact isCountablyGenerated_pure x
  · rcases exists_countable_basis α with ⟨b, b_count, b_ne, hb⟩
    have : Countable b := by exact Iff.mpr countable_coe_iff b_count
    have A : ∀ (s : b), ∃ (x : α), x ∈ (s : Set α) := by
      intro s
      have : (s : Set α) ≠ ∅ := by
        intro H
        apply b_ne
        convert s.2
        exact H.symm
      exact Iff.mp nmem_singleton_empty this
    choose a ha using A
    have : (atTop : Filter α) = (generate (IciIci '' (range a))) := by
      apply atTop_eq_generate_of_not_bddAbove
      intro ⟨x, hx⟩
      simp only [IsTop, not_exists, not_forall, not_le] at h
      rcases h x with ⟨y, hy⟩
      obtain ⟨s, sb, -, hs⟩ : ∃ s, s ∈ b ∧ y ∈ s ∧ s ⊆ Ioi x :=
        hb.exists_subset_of_mem_open hy isOpen_Ioi
      have I : a ⟨s, sb⟩ ≤ x := hx (mem_range_self _)
      have J : x < a ⟨s, sb⟩ := hs (ha ⟨s, sb⟩)
      exact lt_irrefl _ (I.trans_lt J)
    rw [this]
    exact ⟨_, (countable_range _).image _, rfl⟩

Countable Generation of the atTop Filter in Order Topologies

Informal description

For any topological space $\alpha$ with an order topology and a second-countable topology, the filter `atTop` (consisting of all neighborhoods of infinity) is countably generated.

instIsCountablyGenerated_atBot instance

[OrderTopology α] [SecondCountableTopology α] : IsCountablyGenerated (atBot : Filter α)

Full source

instance instIsCountablyGenerated_atBot [OrderTopology α] [SecondCountableTopology α] :
    IsCountablyGenerated (atBot : Filter α) :=
  @instIsCountablyGenerated_atTop αᵒᵈ _ _ _ _

Countable Generation of the atBot Filter in Order Topologies

Informal description

For any topological space $\alpha$ with an order topology and a second-countable topology, the filter `atBot` (consisting of all neighborhoods of negative infinity) is countably generated.

pi_Iic_mem_nhds theorem

(ha : ∀ i, x i < a i) : Iic a ∈ 𝓝 x

Full source

theorem pi_Iic_mem_nhds (ha : ∀ i, x i < a i) : IicIic a ∈ 𝓝 x :=
  pi_univ_Iic a ▸ set_pi_mem_nhds (Set.toFinite _) fun _ _ => Iic_mem_nhds (ha _)

Neighborhood Property of Product of Left-Infinite Right-Closed Intervals

Informal description

For a family of topological spaces $\alpha_i$ indexed by $i \in I$ with order topologies, and points $x, a \in \prod_{i \in I} \alpha_i$, if $x_i < a_i$ for every $i \in I$, then the left-infinite right-closed interval $(-\infty, a]$ is a neighborhood of $x$ in the product topology. That is, there exists an open set containing $x$ that is entirely contained within $(-\infty, a]$.

pi_Iic_mem_nhds' theorem

(ha : ∀ i, x' i < a' i) : Iic a' ∈ 𝓝 x'

Full source

theorem pi_Iic_mem_nhds' (ha : ∀ i, x' i < a' i) : IicIic a' ∈ 𝓝 x' :=
  pi_Iic_mem_nhds ha

Neighborhood property of product of left-infinite right-closed intervals (non-dependent version)

Informal description

For a family of topological spaces $\{\alpha_i\}_{i \in I}$ with order topologies and points $x', a' \in \prod_{i \in I} \alpha_i$, if $x'_i < a'_i$ for every $i \in I$, then the left-infinite right-closed interval $(-\infty, a']$ is a neighborhood of $x'$ in the product topology.

pi_Ici_mem_nhds theorem

(ha : ∀ i, a i < x i) : Ici a ∈ 𝓝 x

Full source

theorem pi_Ici_mem_nhds (ha : ∀ i, a i < x i) : IciIci a ∈ 𝓝 x :=
  pi_univ_Ici a ▸ set_pi_mem_nhds (Set.toFinite _) fun _ _ => Ici_mem_nhds (ha _)

Neighborhood Property of Product of Left-Closed Right-Infinite Intervals

Informal description

For a family of topological spaces $\alpha_i$ indexed by $i \in I$ and a point $x \in \prod_{i \in I} \alpha_i$, if for every index $i$ the element $a_i$ is strictly less than $x_i$ in the order on $\alpha_i$, then the left-closed right-infinite interval $[a, \infty)$ is a neighborhood of $x$ in the product topology. That is, under the given condition, there exists an open set containing $x$ that is entirely contained within $[a, \infty)$.

pi_Ici_mem_nhds' theorem

(ha : ∀ i, a' i < x' i) : Ici a' ∈ 𝓝 x'

Full source

theorem pi_Ici_mem_nhds' (ha : ∀ i, a' i < x' i) : IciIci a' ∈ 𝓝 x' :=
  pi_Ici_mem_nhds ha

Neighborhood property of product of left-closed right-infinite intervals (non-dependent version)

Informal description

For a family of topological spaces $\{\alpha_i\}_{i \in I}$ and a point $x' \in \prod_{i \in I} \alpha_i$, if for every index $i$ the element $a'_i$ is strictly less than $x'_i$ in the order on $\alpha_i$, then the left-closed right-infinite interval $[a', \infty)$ is a neighborhood of $x'$ in the product topology.

pi_Icc_mem_nhds theorem

(ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Icc a b ∈ 𝓝 x

Full source

theorem pi_Icc_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : IccIcc a b ∈ 𝓝 x :=
  pi_univ_Icc a b ▸ set_pi_mem_nhds finite_univ fun _ _ => Icc_mem_nhds (ha _) (hb _)

Closed Interval is a Neighborhood in Product Order Topology

Informal description

For a family of topological spaces $\{\alpha_i\}_{i \in I}$ with order topologies and a point $x = (x_i)_{i \in I}$ in the product space $\prod_{i \in I} \alpha_i$, if for every index $i$ the inequalities $a_i < x_i < b_i$ hold, then the closed interval $[a, b] = \prod_{i \in I} [a_i, b_i]$ is a neighborhood of $x$ in the product topology.

pi_Icc_mem_nhds' theorem

(ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : Icc a' b' ∈ 𝓝 x'

Full source

theorem pi_Icc_mem_nhds' (ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : IccIcc a' b' ∈ 𝓝 x' :=
  pi_Icc_mem_nhds ha hb

Closed Interval is a Neighborhood in Product Order Topology (Non-dependent Version)

Informal description

For a family of topological spaces $\{\alpha_i\}_{i \in I}$ with order topologies and a point $x' = (x'_i)_{i \in I}$ in the product space $\prod_{i \in I} \alpha_i$, if for every index $i$ the inequalities $a'_i < x'_i < b'_i$ hold, then the closed interval $[a', b'] = \prod_{i \in I} [a'_i, b'_i]$ is a neighborhood of $x'$ in the product topology.

pi_Iio_mem_nhds theorem

(ha : ∀ i, x i < a i) : Iio a ∈ 𝓝 x

Full source

theorem pi_Iio_mem_nhds (ha : ∀ i, x i < a i) : IioIio a ∈ 𝓝 x := mem_of_superset
  (set_pi_mem_nhds finite_univ fun i _ ↦ Iio_mem_nhds (ha i)) (pi_univ_Iio_subset a)

Product of Left-Infinite Intervals is a Neighborhood in Product Space

Informal description

For a family of preordered topological spaces $\{\alpha_i\}_{i \in \iota}$ and a point $x = (x_i)_{i \in \iota}$ in the product space $\prod_{i \in \iota} \alpha_i$, if for every index $i$, $x_i < a_i$, then the left-infinite right-open interval $(-\infty, a) = \prod_{i \in \iota} (-\infty, a_i)$ is a neighborhood of $x$ in the product topology.

pi_Iio_mem_nhds' theorem

(ha : ∀ i, x' i < a' i) : Iio a' ∈ 𝓝 x'

Full source

theorem pi_Iio_mem_nhds' (ha : ∀ i, x' i < a' i) : IioIio a' ∈ 𝓝 x' :=
  pi_Iio_mem_nhds ha

Product of Left-Infinite Intervals is a Neighborhood in Product Space (Non-dependent Version)

Informal description

For a family of preordered topological spaces $\{\alpha_i\}_{i \in \iota}$ and a point $x' = (x'_i)_{i \in \iota}$ in the product space $\prod_{i \in \iota} \alpha_i$, if for every index $i$, $x'_i < a'_i$, then the left-infinite right-open interval $(-\infty, a') = \prod_{i \in \iota} (-\infty, a'_i)$ is a neighborhood of $x'$ in the product topology.

pi_Ioi_mem_nhds theorem

(ha : ∀ i, a i < x i) : Ioi a ∈ 𝓝 x

Full source

theorem pi_Ioi_mem_nhds (ha : ∀ i, a i < x i) : IoiIoi a ∈ 𝓝 x :=
  pi_Iio_mem_nhds (π := fun i => (π i)ᵒᵈ) ha

Product of Right-Infinite Intervals is a Neighborhood in Product Space

Informal description

For a family of preordered topological spaces $\{\alpha_i\}_{i \in \iota}$ and a point $x = (x_i)_{i \in \iota}$ in the product space $\prod_{i \in \iota} \alpha_i$, if for every index $i$, $a_i < x_i$, then the right-infinite left-open interval $(a, \infty) = \prod_{i \in \iota} (a_i, \infty)$ is a neighborhood of $x$ in the product topology.

pi_Ioi_mem_nhds' theorem

(ha : ∀ i, a' i < x' i) : Ioi a' ∈ 𝓝 x'

Full source

theorem pi_Ioi_mem_nhds' (ha : ∀ i, a' i < x' i) : IoiIoi a' ∈ 𝓝 x' :=
  pi_Ioi_mem_nhds ha

Product of Right-Infinite Intervals is a Neighborhood in Product Space (Non-dependent Version)

Informal description

For a family of preordered topological spaces $\{\alpha_i\}_{i \in \iota}$ and a point $x' = (x'_i)_{i \in \iota}$ in the product space $\prod_{i \in \iota} \alpha_i$, if for every index $i$, $a'_i < x'_i$, then the right-infinite left-open interval $(a', \infty) = \prod_{i \in \iota} (a'_i, \infty)$ is a neighborhood of $x'$ in the product topology.

pi_Ioc_mem_nhds theorem

(ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Ioc a b ∈ 𝓝 x

Full source

theorem pi_Ioc_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : IocIoc a b ∈ 𝓝 x := by
  refine mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => ?_) (pi_univ_Ioc_subset a b)
  exact Ioc_mem_nhds (ha i) (hb i)

Product of Left-Open Right-Closed Intervals is a Neighborhood in Product Space

Informal description

For a family of preordered topological spaces $\{\alpha_i\}_{i \in \iota}$ and a point $x = (x_i)_{i \in \iota}$ in the product space $\prod_{i \in \iota} \alpha_i$, if for every index $i$, $a_i < x_i < b_i$, then the left-open right-closed interval $\prod_{i \in \iota} (a_i, b_i]$ is a neighborhood of $x$ in the product topology.

pi_Ioc_mem_nhds' theorem

(ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : Ioc a' b' ∈ 𝓝 x'

Full source

theorem pi_Ioc_mem_nhds' (ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : IocIoc a' b' ∈ 𝓝 x' :=
  pi_Ioc_mem_nhds ha hb

Neighborhood Property of Product of Left-Open Right-Closed Intervals (Non-dependent Version)

Informal description

For a family of preordered topological spaces $\{\alpha_i\}_{i \in \iota}$ and a point $x' = (x'_i)_{i \in \iota}$ in the product space $\prod_{i \in \iota} \alpha_i$, if for every index $i$, $a'_i < x'_i < b'_i$, then the left-open right-closed interval $\prod_{i \in \iota} (a'_i, b'_i]$ is a neighborhood of $x'$ in the product topology.

pi_Ico_mem_nhds theorem

(ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Ico a b ∈ 𝓝 x

Full source

theorem pi_Ico_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : IcoIco a b ∈ 𝓝 x := by
  refine mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => ?_) (pi_univ_Ico_subset a b)
  exact Ico_mem_nhds (ha i) (hb i)

Product of Left-Closed Right-Open Intervals is a Neighborhood in Order Topology

Informal description

Let $\{α_i\}_{i \in \iota}$ be a family of preordered topological spaces with the order topology, and let $x = (x_i)_{i \in \iota}$ be a point in the product space $\prod_{i \in \iota} α_i$. If for each index $i$, we have $a_i < x_i < b_i$, then the left-closed right-open interval $\prod_{i \in \iota} [a_i, b_i)$ is a neighborhood of $x$ in the product topology.

pi_Ico_mem_nhds' theorem

(ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : Ico a' b' ∈ 𝓝 x'

Full source

theorem pi_Ico_mem_nhds' (ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : IcoIco a' b' ∈ 𝓝 x' :=
  pi_Ico_mem_nhds ha hb

Product of Left-Closed Right-Open Intervals is a Neighborhood (Non-dependent Version)

Informal description

Let $\{α_i\}_{i \in \iota}$ be a family of preordered topological spaces with the order topology, and let $x' = (x'_i)_{i \in \iota}$ be a point in the product space $\prod_{i \in \iota} α_i$. If for each index $i$, the inequalities $a'_i < x'_i < b'_i$ hold, then the product of left-closed right-open intervals $\prod_{i \in \iota} [a'_i, b'_i)$ is a neighborhood of $x'$ in the product topology.

pi_Ioo_mem_nhds theorem

(ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Ioo a b ∈ 𝓝 x

Full source

theorem pi_Ioo_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : IooIoo a b ∈ 𝓝 x := by
  refine mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => ?_) (pi_univ_Ioo_subset a b)
  exact Ioo_mem_nhds (ha i) (hb i)

Product of Open Intervals is a Neighborhood in Order Topology

Informal description

Let $\{α_i\}_{i \in \iota}$ be a family of preordered topological spaces with the order topology, and let $x = (x_i)_{i \in \iota}$ be a point in the product space $\prod_{i \in \iota} α_i$. If for each index $i$, we have $a_i < x_i < b_i$, then the open interval $\prod_{i \in \iota} (a_i, b_i)$ is a neighborhood of $x$ in the product topology.

pi_Ioo_mem_nhds' theorem

(ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : Ioo a' b' ∈ 𝓝 x'

Full source

theorem pi_Ioo_mem_nhds' (ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : IooIoo a' b' ∈ 𝓝 x' :=
  pi_Ioo_mem_nhds ha hb

Product of Open Intervals is a Neighborhood in Order Topology (Non-dependent Version)

Informal description

Let $\{α_i\}_{i \in \iota}$ be a family of preordered topological spaces with the order topology, and let $x' = (x'_i)_{i \in \iota}$ be a point in the product space $\prod_{i \in \iota} α_i$. If for each index $i$, we have $a'_i < x'_i < b'_i$, then the open interval $\prod_{i \in \iota} (a'_i, b'_i)$ is a neighborhood of $x'$ in the product topology.

Mathlib.Topology.Order.Basic

Main definitions

Main statements

Implementation notes