Documentation

Mathlib.Topology.Order.Basic

Theory of topology on ordered spaces #

Main definitions #

The order topology on an ordered space is the topology generated by all open intervals (or equivalently by those of the form (-∞, a) and (b, +∞)). We define it as Preorder.topology α. However, we do not register it as an instance (as many existing ordered types already have topologies, which would be equal but not definitionally equal to Preorder.topology α). Instead, we introduce a class OrderTopology α (which is a Prop, also known as a mixin) saying that on the type α having already a topological space structure and a preorder structure, the topological structure is equal to the order topology.

We prove many basic properties of such topologies.

Main statements #

This file contains the proofs of the following facts. For exact requirements (OrderClosedTopology vs OrderTopology, Preorder vs PartialOrder vs LinearOrder etc) see their statements.

Implementation notes #

We do not register the order topology as an instance on a preorder (or even on a linear order). Indeed, on many such spaces, a topology has already been constructed in a different way (think of the discrete spaces or , or that could inherit a topology as the completion of ), and is in general not defeq to the one generated by the intervals. We make it available as a definition Preorder.topology α though, that can be registered as an instance when necessary, or for specific types.

class OrderTopology (α : Type u_1) [t : TopologicalSpace α] [Preorder α] :

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.

Instances
    theorem OrderTopology.topology_eq_generate_intervals {α : Type u_1} {t : TopologicalSpace α} :
    ∀ {inst : Preorder α} [self : OrderTopology α], t = TopologicalSpace.generateFrom {s : Set α | ∃ (a : α), s = Set.Ioi a s = Set.Iio a}

    The topology is generated by open intervals Set.Ioi _ and Set.Iio _.

    (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.

    Equations
    Instances For
      Equations
      • =
      theorem isOpen_iff_generate_intervals {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderTopology α] {s : Set α} :
      IsOpen s TopologicalSpace.GenerateOpen {s : Set α | ∃ (a : α), s = Set.Ioi a s = Set.Iio a} s
      theorem isOpen_lt' {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
      IsOpen {b : α | a < b}
      theorem isOpen_gt' {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
      IsOpen {b : α | b < a}
      theorem lt_mem_nhds {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} {b : α} (h : a < b) :
      ∀ᶠ (x : α) in nhds b, a < x
      theorem le_mem_nhds {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} {b : α} (h : a < b) :
      ∀ᶠ (x : α) in nhds b, a x
      theorem gt_mem_nhds {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} {b : α} (h : a < b) :
      ∀ᶠ (x : α) in nhds a, x < b
      theorem ge_mem_nhds {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} {b : α} (h : a < b) :
      ∀ᶠ (x : α) in nhds a, x b
      theorem nhds_eq_order {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
      nhds a = (⨅ bSet.Iio a, Filter.principal (Set.Ioi b)) bSet.Ioi a, Filter.principal (Set.Iio b)
      theorem tendsto_order {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [OrderTopology α] {f : βα} {a : α} {x : Filter β} :
      Filter.Tendsto f x (nhds a) (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) a' > a, ∀ᶠ (b : β) in x, f b < a'
      instance tendstoIccClassNhds {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
      Equations
      • =
      instance tendstoIcoClassNhds {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
      Equations
      • =
      instance tendstoIocClassNhds {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
      Equations
      • =
      instance tendstoIooClassNhds {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
      Equations
      • =
      theorem tendsto_of_tendsto_of_tendsto_of_le_of_le' {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [OrderTopology α] {f : βα} {g : βα} {h : βα} {b : Filter β} {a : α} (hg : Filter.Tendsto g b (nhds a)) (hh : Filter.Tendsto h b (nhds a)) (hgf : ∀ᶠ (b : β) in b, g b f b) (hfh : ∀ᶠ (b : β) in b, f b h b) :

      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 {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [OrderTopology α] {f : βα} {g : βα} {h : βα} {b : Filter β} {a : α} (hg : Filter.Tendsto g b (nhds a)) (hh : Filter.Tendsto h b (nhds a)) (hgf : g f) (hfh : f h) :

      Squeeze theorem (also known as sandwich theorem). This version assumes that inequalities hold everywhere.

      theorem nhds_order_unbounded {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} (hu : ∃ (u : α), a < u) (hl : ∃ (l : α), l < a) :
      nhds a = ⨅ (l : α), ⨅ (_ : l < a), ⨅ (u : α), ⨅ (_ : a < u), Filter.principal (Set.Ioo l u)
      theorem tendsto_order_unbounded {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [OrderTopology α] {f : βα} {a : α} {x : Filter β} (hu : ∃ (u : α), a < u) (hl : ∃ (l : α), l < a) (h : ∀ (l u : α), l < aa < u∀ᶠ (b : β) in x, l < f b f b < u) :
      instance tendstoIxxNhdsWithin {α : Type u_1} [TopologicalSpace α] (a : α) {s : Set α} {t : Set α} {Ixx : ααSet α} [Filter.TendstoIxxClass Ixx (nhds a) (nhds a)] [Filter.TendstoIxxClass Ixx (Filter.principal s) (Filter.principal t)] :
      Equations
      • =
      instance tendstoIccClassNhdsPi {ι : Type u_1} {α : ιType u_2} [(i : ι) → Preorder (α i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), OrderTopology (α i)] (f : (i : ι) → α i) :
      Equations
      • =
      theorem induced_topology_le_preorder {α : Type u} {β : Type v} [Preorder α] [Preorder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} (hf : ∀ {x y : α}, f x < f y x < y) :
      theorem induced_topology_eq_preorder {α : Type u} {β : Type v} [Preorder α] [Preorder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} (hf : ∀ {x y : α}, f x < f y x < y) (H₁ : ∀ {a : α} {b : β} {x : α}, b < f a¬b < f xy < a, b f y) (H₂ : ∀ {a : α} {b : β} {x : α}, f a < b¬f x < b∃ (y : α), a < y f y b) :
      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 ab < a, x f b) (H₂ : ∀ {a : α} {x : β}, f a < xb > a, f b x) :
      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) :
      theorem StrictMono.induced_topology_eq_preorder {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] [t : TopologicalSpace β] [OrderTopology β] {f : αβ} (hf : StrictMono f) (hc : (Set.range f).OrdConnected) :

      The topology induced by a strictly monotone function with order-connected range is the preorder topology.

      theorem StrictMono.embedding_of_ordConnected {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] [TopologicalSpace α] [h : OrderTopology α] [TopologicalSpace β] [OrderTopology β] {f : αβ} (hf : StrictMono f) (hc : (Set.range f).OrdConnected) :

      A strictly monotone function between linear orders with order topology is a topological embedding provided that the range of f is order-connected.

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

      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.

      Equations
      • =
      theorem nhdsWithin_Ici_eq'' {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
      nhdsWithin a (Set.Ici a) = (⨅ (u : α), ⨅ (_ : a < u), Filter.principal (Set.Iio u)) Filter.principal (Set.Ici a)
      theorem nhdsWithin_Iic_eq'' {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
      nhdsWithin a (Set.Iic a) = (⨅ (l : α), ⨅ (_ : l < a), Filter.principal (Set.Ioi l)) Filter.principal (Set.Iic a)
      theorem nhdsWithin_Ici_eq' {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} (ha : ∃ (u : α), a < u) :
      nhdsWithin a (Set.Ici a) = ⨅ (u : α), ⨅ (_ : a < u), Filter.principal (Set.Ico a u)
      theorem nhdsWithin_Iic_eq' {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} (ha : ∃ (l : α), l < a) :
      nhdsWithin a (Set.Iic a) = ⨅ (l : α), ⨅ (_ : l < a), Filter.principal (Set.Ioc l a)
      theorem nhdsWithin_Ici_basis' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (ha : ∃ (u : α), a < u) :
      (nhdsWithin a (Set.Ici a)).HasBasis (fun (u : α) => a < u) fun (u : α) => Set.Ico a u
      theorem nhdsWithin_Iic_basis' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (ha : ∃ (l : α), l < a) :
      (nhdsWithin a (Set.Iic a)).HasBasis (fun (l : α) => l < a) fun (l : α) => Set.Ioc l a
      theorem nhdsWithin_Ici_basis {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α) :
      (nhdsWithin a (Set.Ici a)).HasBasis (fun (u : α) => a < u) fun (u : α) => Set.Ico a u
      theorem nhdsWithin_Iic_basis {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] (a : α) :
      (nhdsWithin a (Set.Iic a)).HasBasis (fun (l : α) => l < a) fun (l : α) => Set.Ioc l a
      theorem nhds_top_order {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTop α] [OrderTopology α] :
      nhds = ⨅ (l : α), ⨅ (_ : l < ), Filter.principal (Set.Ioi l)
      theorem nhds_bot_order {α : Type u} [TopologicalSpace α] [Preorder α] [OrderBot α] [OrderTopology α] :
      nhds = ⨅ (l : α), ⨅ (_ : < l), Filter.principal (Set.Iio l)
      theorem nhds_top_basis {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α] [Nontrivial α] :
      (nhds ).HasBasis (fun (a : α) => a < ) fun (a : α) => Set.Ioi a
      theorem nhds_bot_basis {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α] [Nontrivial α] :
      (nhds ).HasBasis (fun (a : α) => < a) fun (a : α) => Set.Iio a
      theorem nhds_top_basis_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α] [Nontrivial α] [DenselyOrdered α] :
      (nhds ).HasBasis (fun (a : α) => a < ) Set.Ici
      theorem nhds_bot_basis_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α] [Nontrivial α] [DenselyOrdered α] :
      (nhds ).HasBasis (fun (a : α) => < a) Set.Iic
      theorem tendsto_nhds_top_mono {α : Type u} {β : Type v} [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β] {l : Filter α} {f : αβ} {g : αβ} (hf : Filter.Tendsto f l (nhds )) (hg : f ≤ᶠ[l] g) :
      theorem tendsto_nhds_bot_mono {α : Type u} {β : Type v} [TopologicalSpace β] [Preorder β] [OrderBot β] [OrderTopology β] {l : Filter α} {f : αβ} {g : αβ} (hf : Filter.Tendsto f l (nhds )) (hg : g ≤ᶠ[l] f) :
      theorem tendsto_nhds_top_mono' {α : Type u} {β : Type v} [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β] {l : Filter α} {f : αβ} {g : αβ} (hf : Filter.Tendsto f l (nhds )) (hg : f g) :
      theorem tendsto_nhds_bot_mono' {α : Type u} {β : Type v} [TopologicalSpace β] [Preorder β] [OrderBot β] [OrderTopology β] {l : Filter α} {f : αβ} {g : αβ} (hf : Filter.Tendsto f l (nhds )) (hg : g f) :
      theorem order_separated {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a₁ : α} {a₂ : α} (h : a₁ < a₂) :
      ∃ (u : Set α) (v : Set α), IsOpen u IsOpen v a₁ u a₂ v b₁u, b₂v, b₁ < b₂
      @[instance 100]
      Equations
      • =
      theorem exists_Ioc_subset_of_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s nhds a) (h : ∃ (l : α), l < a) :
      l < a, Set.Ioc l a s
      theorem exists_Ioc_subset_of_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s nhds a) {l : α} (hl : l < a) :
      l'Set.Ico l a, Set.Ioc l' a s
      theorem exists_Ico_subset_of_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s nhds a) {u : α} (hu : a < u) :
      u'Set.Ioc a u, Set.Ico a u' s
      theorem exists_Ico_subset_of_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s nhds a) (h : ∃ (u : α), a < u) :
      ∃ (u : α), a < u Set.Ico a u s
      theorem exists_Icc_mem_subset_of_mem_nhdsWithin_Ici {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s nhdsWithin a (Set.Ici a)) :
      ∃ (b : α), a b Set.Icc a b nhdsWithin a (Set.Ici a) Set.Icc a b s
      theorem exists_Icc_mem_subset_of_mem_nhdsWithin_Iic {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s nhdsWithin a (Set.Iic a)) :
      ba, Set.Icc b a nhdsWithin a (Set.Iic a) Set.Icc b a s
      theorem exists_Icc_mem_subset_of_mem_nhds {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s nhds a) :
      ∃ (b : α) (c : α), a Set.Icc b c Set.Icc b c nhds a Set.Icc b c s
      theorem IsOpen.exists_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Nontrivial α] {s : Set α} (hs : IsOpen s) (h : s.Nonempty) :
      ∃ (a : α) (b : α), a < b Set.Ioo a b s
      theorem dense_of_exists_between {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Nontrivial α] {s : Set α} (h : ∀ ⦃a b : α⦄, a < bcs, a < c c < b) :
      theorem dense_iff_exists_between {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [Nontrivial α] {s : Set α} :
      Dense s ∀ (a b : α), a < bcs, a < c c < b

      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 mem_nhds_iff_exists_Ioo_subset' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hl : ∃ (l : α), l < a) (hu : ∃ (u : α), a < u) :
      s nhds a ∃ (l : α) (u : α), a Set.Ioo l u Set.Ioo l u s

      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 {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] {a : α} {s : Set α} :
      s nhds a ∃ (l : α) (u : α), a Set.Ioo l u Set.Ioo l u s

      A set is a neighborhood of a if and only if it contains an interval (l, u) containing a.

      theorem nhds_basis_Ioo' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (hl : ∃ (l : α), l < a) (hu : ∃ (u : α), a < u) :
      (nhds a).HasBasis (fun (b : α × α) => b.1 < a a < b.2) fun (b : α × α) => Set.Ioo b.1 b.2
      theorem nhds_basis_Ioo {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] (a : α) :
      (nhds a).HasBasis (fun (b : α × α) => b.1 < a a < b.2) fun (b : α × α) => Set.Ioo b.1 b.2
      theorem Filter.Eventually.exists_Ioo_subset {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] {a : α} {p : αProp} (hp : ∀ᶠ (x : α) in nhds a, p x) :
      ∃ (l : α) (u : α), a Set.Ioo l u Set.Ioo l u {x : α | p x}
      theorem Dense.topology_eq_generateFrom {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {s : Set α} (hs : Dense s) :
      inst✝³ = TopologicalSpace.generateFrom (Set.Ioi '' s Set.Iio '' s)
      @[deprecated Filter.OrderBot.atBot_eq]
      theorem atBot_le_nhds_bot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderBot α] :
      Filter.atBot nhds
      @[deprecated Filter.OrderTop.atTop_eq]
      theorem atTop_le_nhds_top {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTop α] :
      Filter.atTop nhds

      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 for a counterexample.

      theorem countable_setOf_covBy_right {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] :
      {x : α | ∃ (y : α), x y}.Countable

      The set of points which are isolated on the right is countable when the space is second-countable.

      theorem countable_setOf_covBy_left {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] :
      {x : α | ∃ (y : α), y x}.Countable

      The set of points which are isolated on the left is countable when the space is second-countable.

      theorem countable_of_isolated_left' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] :
      {x : α | y < x, Set.Ioo y x = }.Countable

      The set of points which are isolated on the left is countable when the space is second-countable.

      theorem Set.PairwiseDisjoint.countable_of_Ioo {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {y : αα} {s : Set α} (h : s.PairwiseDisjoint fun (x : α) => Set.Ioo x (y x)) (h' : xs, x < y x) :
      s.Countable

      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 countable_image_lt_image_Ioi {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] (f : βα) [SecondCountableTopology α] :
      {x : β | ∃ (z : α), f x < z ∀ (y : β), x < yz f y}.Countable

      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_gt_image_Ioi {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] (f : βα) [SecondCountableTopology α] :
      {x : β | z < f x, ∀ (y : β), x < yf y z}.Countable

      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_lt_image_Iio {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] (f : βα) [SecondCountableTopology α] :
      {x : β | ∃ (z : α), f x < z y < x, z f y}.Countable

      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_gt_image_Iio {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] (f : βα) [SecondCountableTopology α] :
      {x : β | z < f x, y < x, f y z}.Countable

      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.

      instance instIsCountablyGenerated_atTop {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] :
      Filter.atTop.IsCountablyGenerated
      Equations
      • =
      instance instIsCountablyGenerated_atBot {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] :
      Filter.atBot.IsCountablyGenerated
      Equations
      • =

      Intervals in Π i, π i belong to 𝓝 x #

      For each lemma pi_Ixx_mem_nhds we add a non-dependent version pi_Ixx_mem_nhds' because sometimes Lean fails to unify different instances while trying to apply the dependent version to, e.g., ι → ℝ.

      theorem pi_Iic_mem_nhds {ι : Type u_1} {π : ιType u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {x : (i : ι) → π i} (ha : ∀ (i : ι), x i < a i) :
      theorem pi_Iic_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' : ια} {x' : ια} (ha : ∀ (i : ι), x' i < a' i) :
      theorem pi_Ici_mem_nhds {ι : Type u_1} {π : ιType u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {x : (i : ι) → π i} (ha : ∀ (i : ι), a i < x i) :
      theorem pi_Ici_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' : ια} {x' : ια} (ha : ∀ (i : ι), a' i < x' i) :
      theorem pi_Icc_mem_nhds {ι : Type u_1} {π : ιType u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} {x : (i : ι) → π i} (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) :
      theorem pi_Icc_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' : ια} {b' : ια} {x' : ια} (ha : ∀ (i : ι), a' i < x' i) (hb : ∀ (i : ι), x' i < b' i) :
      Set.Icc a' b' nhds x'
      theorem pi_Iio_mem_nhds {ι : Type u_1} {π : ιType u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {x : (i : ι) → π i} [Nonempty ι] (ha : ∀ (i : ι), x i < a i) :
      theorem pi_Iio_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' : ια} {x' : ια} [Nonempty ι] (ha : ∀ (i : ι), x' i < a' i) :
      theorem pi_Ioi_mem_nhds {ι : Type u_1} {π : ιType u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {x : (i : ι) → π i} [Nonempty ι] (ha : ∀ (i : ι), a i < x i) :
      theorem pi_Ioi_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' : ια} {x' : ια} [Nonempty ι] (ha : ∀ (i : ι), a' i < x' i) :
      theorem pi_Ioc_mem_nhds {ι : Type u_1} {π : ιType u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} {x : (i : ι) → π i} [Nonempty ι] (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) :
      theorem pi_Ioc_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' : ια} {b' : ια} {x' : ια} [Nonempty ι] (ha : ∀ (i : ι), a' i < x' i) (hb : ∀ (i : ι), x' i < b' i) :
      Set.Ioc a' b' nhds x'
      theorem pi_Ico_mem_nhds {ι : Type u_1} {π : ιType u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} {x : (i : ι) → π i} [Nonempty ι] (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) :
      theorem pi_Ico_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' : ια} {b' : ια} {x' : ια} [Nonempty ι] (ha : ∀ (i : ι), a' i < x' i) (hb : ∀ (i : ι), x' i < b' i) :
      Set.Ico a' b' nhds x'
      theorem pi_Ioo_mem_nhds {ι : Type u_1} {π : ιType u_2} [Finite ι] [(i : ι) → LinearOrder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), OrderTopology (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} {x : (i : ι) → π i} [Nonempty ι] (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) :
      theorem pi_Ioo_mem_nhds' {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' : ια} {b' : ια} {x' : ια} [Nonempty ι] (ha : ∀ (i : ι), a' i < x' i) (hb : ∀ (i : ι), x' i < b' i) :
      Set.Ioo a' b' nhds x'