Filter.atTop and Filter.atBot for intervals in a linear order topology #
Let X be a linear order with order topology.
Let a be a point that is either the bottom element of X or is not isolated on the left,
see Order.IsSuccPrelimit.
Then the Filter.atTop filter on Set.Iio a and 𝓝[<] a are related by the coercion map
via pushforward and pullback, see map_coe_Iio_atTop and comap_coe_Iio_nhdsLT.
We prove several versions of this statement for Set.Iio, Set.Ioi, and Set.Ioo,
as well as Filter.atTop and Filter.atBot.
The assumption on a is automatically satisfied for densely ordered types,
see Order.IsSuccPrelimit.of_dense.
theorem
comap_coe_nhdsLT_eq_atTop_iff
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{s : Set X}
{b : X}
:
Filter.comap Subtype.val (nhdsWithin b (Set.Iio b)) = Filter.atTop ↔ s ⊆ Set.Iio b ∧ (s.Nonempty → ∀ a < b, (s ∩ Set.Ioo a b).Nonempty)
theorem
comap_coe_nhdsGT_eq_atBot_iff
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{s : Set X}
{b : X}
:
Filter.comap Subtype.val (nhdsWithin b (Set.Ioi b)) = Filter.atBot ↔ s ⊆ Set.Ioi b ∧ (s.Nonempty → ∀ a > b, (s ∩ Set.Ioo b a).Nonempty)
theorem
comap_coe_nhdsLT_of_Ioo_subset
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{s : Set X}
{b : X}
(hsb : s ⊆ Set.Iio b)
(hs : s.Nonempty → ∃ a < b, Set.Ioo a b ⊆ s)
(hb : Order.IsSuccPrelimit b := by exact .of_dense _)
:
theorem
comap_coe_nhdsGT_of_Ioo_subset
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{s : Set X}
{a : X}
(hsa : s ⊆ Set.Ioi a)
(hs : s.Nonempty → ∃ b > a, Set.Ioo a b ⊆ s)
(ha : Order.IsPredPrelimit a := by exact .of_dense _)
:
theorem
map_coe_atTop_of_Ioo_subset
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{s : Set X}
{b : X}
(hsb : s ⊆ Set.Iio b)
(hs : ∀ a' < b, ∃ a < b, Set.Ioo a b ⊆ s)
(hb : Order.IsSuccPrelimit b := by exact .of_dense _)
:
theorem
map_coe_atBot_of_Ioo_subset
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{s : Set X}
{a : X}
(hsa : s ⊆ Set.Ioi a)
(hs : ∀ b' > a, ∃ b > a, Set.Ioo a b ⊆ s)
(ha : Order.IsPredPrelimit a := by exact .of_dense _)
:
@[simp]
theorem
comap_coe_Ioo_nhdsLT
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
(a b : X)
(hb : Order.IsSuccPrelimit b := by exact .of_dense _)
:
The atTop filter for an open interval Ioo a b comes from the left-neighbourhoods filter at
the right endpoint in the ambient order.
@[simp]
theorem
comap_coe_Ioo_nhdsGT
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
(a b : X)
(ha : Order.IsPredPrelimit a := by exact .of_dense _)
:
The atBot filter for an open interval Ioo a b comes from the right-neighbourhoods filter at
the left endpoint in the ambient order.
@[simp]
theorem
comap_coe_Ioi_nhdsGT
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
(a : X)
(ha : Order.IsPredPrelimit a := by exact .of_dense _)
:
@[simp]
theorem
comap_coe_Iio_nhdsLT
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
(a : X)
(ha : Order.IsSuccPrelimit a := by exact .of_dense _)
:
@[simp]
theorem
map_coe_Ioo_atTop
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{a b : X}
(h : a < b)
(hb : Order.IsSuccPrelimit b := by exact .of_dense _)
:
@[simp]
theorem
map_coe_Ioo_atBot
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{a b : X}
(h : a < b)
(ha : Order.IsPredPrelimit a := by exact .of_dense _)
:
@[simp]
theorem
map_coe_Ioi_atBot
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
(a : X)
(ha : Order.IsPredPrelimit a := by exact .of_dense _)
:
@[simp]
theorem
map_coe_Iio_atTop
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
(a : X)
(ha : Order.IsSuccPrelimit a := by exact .of_dense _)
:
@[simp]
theorem
tendsto_comp_coe_Ioo_atTop
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{a b : X}
{α : Type u_2}
{l : Filter α}
{f : X → α}
(h : a < b)
(hb : Order.IsSuccPrelimit b := by exact .of_dense _)
:
Filter.Tendsto (fun (x : ↑(Set.Ioo a b)) => f ↑x) Filter.atTop l ↔ Filter.Tendsto f (nhdsWithin b (Set.Iio b)) l
@[simp]
theorem
tendsto_comp_coe_Ioo_atBot
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{a b : X}
{α : Type u_2}
{l : Filter α}
{f : X → α}
(h : a < b)
(ha : Order.IsPredPrelimit a := by exact .of_dense _)
:
Filter.Tendsto (fun (x : ↑(Set.Ioo a b)) => f ↑x) Filter.atBot l ↔ Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) l
@[simp]
theorem
tendsto_comp_coe_Ioi_atBot
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{a : X}
{α : Type u_2}
{l : Filter α}
{f : X → α}
(ha : Order.IsPredPrelimit a := by exact .of_dense _)
:
Filter.Tendsto (fun (x : ↑(Set.Ioi a)) => f ↑x) Filter.atBot l ↔ Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) l
@[simp]
theorem
tendsto_comp_coe_Iio_atTop
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{a : X}
{α : Type u_2}
{l : Filter α}
{f : X → α}
(ha : Order.IsSuccPrelimit a := by exact .of_dense _)
:
Filter.Tendsto (fun (x : ↑(Set.Iio a)) => f ↑x) Filter.atTop l ↔ Filter.Tendsto f (nhdsWithin a (Set.Iio a)) l
@[simp]
theorem
tendsto_Ioo_atTop
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{a b : X}
{α : Type u_2}
{l : Filter α}
{f : α → ↑(Set.Ioo a b)}
(hb : Order.IsSuccPrelimit b := by exact .of_dense _)
:
Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto (fun (x : α) => ↑(f x)) l (nhdsWithin b (Set.Iio b))
@[simp]
theorem
tendsto_Ioo_atBot
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{a b : X}
{α : Type u_2}
{l : Filter α}
{f : α → ↑(Set.Ioo a b)}
(ha : Order.IsPredPrelimit a := by exact .of_dense _)
:
Filter.Tendsto f l Filter.atBot ↔ Filter.Tendsto (fun (x : α) => ↑(f x)) l (nhdsWithin a (Set.Ioi a))
@[simp]
theorem
tendsto_Ioi_atBot
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{a : X}
{α : Type u_2}
{l : Filter α}
{f : α → ↑(Set.Ioi a)}
(ha : Order.IsPredPrelimit a := by exact .of_dense _)
:
Filter.Tendsto f l Filter.atBot ↔ Filter.Tendsto (fun (x : α) => ↑(f x)) l (nhdsWithin a (Set.Ioi a))
@[simp]
theorem
tendsto_Iio_atTop
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{a : X}
{α : Type u_2}
{l : Filter α}
{f : α → ↑(Set.Iio a)}
(ha : Order.IsSuccPrelimit a := by exact .of_dense _)
:
Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto (fun (x : α) => ↑(f x)) l (nhdsWithin a (Set.Iio a))