Limits of intervals along filters

This file contains some lemmas about how filters Ixx behave as the endpoints tend to ±∞.

theorem Finset.tendsto_Icc_atBot_prod_atTop {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] : Filter.Tendsto (fun (p : α × α) => Icc p.1 p.2) (Filter.atBot ×ˢ Filter.atTop) Filter.atTop

theorem Finset.tendsto_Ioc_atBot_prod_atTop {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] [NoBotOrder α] : Filter.Tendsto (fun (p : α × α) => Ioc p.1 p.2) (Filter.atBot ×ˢ Filter.atTop) Filter.atTop

theorem Finset.tendsto_Ico_atBot_prod_atTop {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] [NoTopOrder α] : Filter.Tendsto (fun (p : α × α) => Ico p.1 p.2) (Filter.atBot ×ˢ Filter.atTop) Filter.atTop

theorem Finset.tendsto_Ioo_atBot_prod_atTop {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] [NoBotOrder α] [NoTopOrder α] : Filter.Tendsto (fun (p : α × α) => Ioo p.1 p.2) (Filter.atBot ×ˢ Filter.atTop) Filter.atTop

theorem Finset.tendsto_Icc_neg_atTop_atTop {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [LocallyFiniteOrder α] : Filter.Tendsto (fun (a : α) => Icc (-a) a) Filter.atTop Filter.atTop

theorem Finset.tendsto_Ioc_neg_atTop_atTop {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [LocallyFiniteOrder α] [NoBotOrder α] : Filter.Tendsto (fun (a : α) => Ioc (-a) a) Filter.atTop Filter.atTop

theorem Finset.tendsto_Ico_neg_atTop_atTop {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [LocallyFiniteOrder α] [NoTopOrder α] : Filter.Tendsto (fun (a : α) => Ico (-a) a) Filter.atTop Filter.atTop

theorem Finset.tendsto_Ioo_neg_atTop_atTop {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [LocallyFiniteOrder α] [NoBotOrder α] [NoTopOrder α] : Filter.Tendsto (fun (a : α) => Ioo (-a) a) Filter.atTop Filter.atTop

theorem Finset.tendsto_Icc_neg {R : Type u_1} [Ring R] [PartialOrder R] [IsOrderedRing R] [LocallyFiniteOrder R] [Archimedean R] : Filter.Tendsto (fun (n : ℕ) => Icc (-↑n) ↑n) Filter.atTop Filter.atTop

theorem Finset.tendsto_Ioc_neg {R : Type u_1} [Ring R] [PartialOrder R] [IsOrderedRing R] [LocallyFiniteOrder R] [Archimedean R] [Nontrivial R] : Filter.Tendsto (fun (n : ℕ) => Ioc (-↑n) ↑n) Filter.atTop Filter.atTop

theorem Finset.tendsto_Ico_neg {R : Type u_1} [Ring R] [PartialOrder R] [IsOrderedRing R] [LocallyFiniteOrder R] [Archimedean R] [Nontrivial R] : Filter.Tendsto (fun (n : ℕ) => Ico (-↑n) ↑n) Filter.atTop Filter.atTop

theorem Finset.tendsto_Ioo_neg {R : Type u_1} [Ring R] [PartialOrder R] [IsOrderedRing R] [LocallyFiniteOrder R] [Archimedean R] [Nontrivial R] : Filter.Tendsto (fun (n : ℕ) => Ioo (-↑n) ↑n) Filter.atTop Filter.atTop