# Documentation

Mathlib.Order.Filter.Interval

# Convergence of intervals #

If both a and b tend to some filter l₁, sometimes this implies that Ixx a b tends to l₂.smallSets, i.e., for any s ∈ l₂ eventually Ixx a b becomes a subset of s. Here and below Ixx is one of Set.Icc, Set.Ico, Set.Ioc, and Set.Ioo. We define Filter.TendstoIxxClass Ixx l₁ l₂ to be a typeclass representing this property.

The instances provide the best l₂ for a given l₁. In many cases l₁ = l₂ but sometimes we can drop an endpoint from an interval: e.g., we prove Filter.TendstoIxxClass Set.Ico (𝓟 (Set.Iic a)) (𝓟 (Set.Iio a)), i.e., if u₁ n and u₂ n belong eventually to Set.Iic a, then the interval Set.Ico (u₁ n) (u₂ n) is eventually included in Set.Iio a.

The next table shows “output” filters l₂ for different values of Ixx and l₁. The instances that need topology are defined in Mathlib/Topology/Algebra/Ordered.

| Input filter | Ixx = Set.Icc | Ixx = Set.Ico | Ixx = Set.Ioc | Ixx = Set.Ioo | |-----------------:|:----------------:|:----------------:|:----------------:|:----------------:| | Filter.atTop | Filter.atTop | Filter.atTop | Filter.atTop | Filter.atTop | | Filter.atBot | Filter.atBot | Filter.atBot | Filter.atBot | Filter.atBot | | pure a | pure a | ⊥ | ⊥ | ⊥ | | 𝓟 (Set.Iic a) | 𝓟 (Set.Iic a) | 𝓟 (Set.Iio a) | 𝓟 (Set.Iic a) | 𝓟 (Set.Iio a) | | 𝓟 (Set.Ici a) | 𝓟 (Set.Ici a) | 𝓟 (Set.Ici a) | 𝓟 (Set.Ioi a) | 𝓟 (Set.Ioi a) | | 𝓟 (Set.Ioi a) | 𝓟 (Set.Ioi a) | 𝓟 (Set.Ioi a) | 𝓟 (Set.Ioi a) | 𝓟 (Set.Ioi a) | | 𝓟 (Set.Iio a) | 𝓟 (Set.Iio a) | 𝓟 (Set.Iio a) | 𝓟 (Set.Iio a) | 𝓟 (Set.Iio a) | | 𝓝 a | 𝓝 a | 𝓝 a | 𝓝 a | 𝓝 a | | 𝓝[Set.Iic a] b | 𝓝[Set.Iic a] b | 𝓝[Set.Iio a] b | 𝓝[Set.Iic a] b | 𝓝[Set.Iio a] b | | 𝓝[Set.Ici a] b | 𝓝[Set.Ici a] b | 𝓝[Set.Ici a] b | 𝓝[Set.Ioi a] b | 𝓝[Set.Ioi a] b | | 𝓝[Set.Ioi a] b | 𝓝[Set.Ioi a] b | 𝓝[Set.Ioi a] b | 𝓝[Set.Ioi a] b | 𝓝[Set.Ioi a] b | | 𝓝[Set.Iio a] b | 𝓝[Set.Iio a] b | 𝓝[Set.Iio a] b | 𝓝[Set.Iio a] b | 𝓝[Set.Iio a] b |

class Filter.TendstoIxxClass {α : Type u_1} (Ixx : ααSet α) (l₁ : ) (l₂ : outParam ()) :
• tendsto_Ixx : Filter.Tendsto (fun p => Ixx p.fst p.snd) (l₁ ×ˢ l₁) ()

Function.uncurry Ixx tends to l₂.smallSets along l₁ ×ˢ l₁. In other words, for any s ∈ l₂ there exists t ∈ l₁ such that Ixx x y ⊆ s whenever x ∈ t and y ∈ t.

Use lemmas like Filter.Tendsto.Icc instead.

A pair of filters l₁, l₂ has TendstoIxxClass Ixx property if Ixx a b tends to l₂.small_sets as a and b tend to l₁. In all instances Ixx is one of Set.Icc, Set.Ico, Set.Ioc, or Set.Ioo. The instances provide the best l₂ for a given l₁. In many cases l₁ = l₂ but sometimes we can drop an endpoint from an interval: e.g., we prove TendstoIxxClass Set.Ico (𝓟 (Set.Iic a)) (𝓟 (Set.Iio a)), i.e., if u₁ n and u₂ n belong eventually to Set.Iic a, then the interval Set.Ico (u₁ n) (u₂ n) is eventually included in Set.Iio a.

We mark l₂ as an outParam so that Lean can automatically find an appropriate l₂ based on Ixx and l₁. This way, e.g., tendsto.Ico h₁ h₂ works without specifying explicitly l₂.

Instances
theorem Filter.Tendsto.Icc {α : Type u_1} {β : Type u_2} [] {l₁ : } {l₂ : } [Filter.TendstoIxxClass Set.Icc l₁ l₂] {lb : } {u₁ : βα} {u₂ : βα} (h₁ : Filter.Tendsto u₁ lb l₁) (h₂ : Filter.Tendsto u₂ lb l₁) :
Filter.Tendsto (fun x => Set.Icc (u₁ x) (u₂ x)) lb ()
theorem Filter.Tendsto.Ioc {α : Type u_1} {β : Type u_2} [] {l₁ : } {l₂ : } [Filter.TendstoIxxClass Set.Ioc l₁ l₂] {lb : } {u₁ : βα} {u₂ : βα} (h₁ : Filter.Tendsto u₁ lb l₁) (h₂ : Filter.Tendsto u₂ lb l₁) :
Filter.Tendsto (fun x => Set.Ioc (u₁ x) (u₂ x)) lb ()
theorem Filter.Tendsto.Ico {α : Type u_1} {β : Type u_2} [] {l₁ : } {l₂ : } [Filter.TendstoIxxClass Set.Ico l₁ l₂] {lb : } {u₁ : βα} {u₂ : βα} (h₁ : Filter.Tendsto u₁ lb l₁) (h₂ : Filter.Tendsto u₂ lb l₁) :
Filter.Tendsto (fun x => Set.Ico (u₁ x) (u₂ x)) lb ()
theorem Filter.Tendsto.Ioo {α : Type u_1} {β : Type u_2} [] {l₁ : } {l₂ : } [Filter.TendstoIxxClass Set.Ioo l₁ l₂] {lb : } {u₁ : βα} {u₂ : βα} (h₁ : Filter.Tendsto u₁ lb l₁) (h₂ : Filter.Tendsto u₂ lb l₁) :
Filter.Tendsto (fun x => Set.Ioo (u₁ x) (u₂ x)) lb ()
theorem Filter.tendstoIxxClass_principal {α : Type u_1} {s : Set α} {t : Set α} {Ixx : ααSet α} :
∀ (x : α), x s∀ (y : α), y sIxx x y t
theorem Filter.tendstoIxxClass_inf {α : Type u_1} {l₁ : } {l₁' : } {l₂ : } {l₂' : } {Ixx : ααSet α} [h : Filter.TendstoIxxClass Ixx l₁ l₂] [h' : Filter.TendstoIxxClass Ixx l₁' l₂'] :
Filter.TendstoIxxClass Ixx (l₁ l₁') (l₂ l₂')
theorem Filter.tendstoIxxClass_of_subset {α : Type u_1} {l₁ : } {l₂ : } {Ixx : ααSet α} {Ixx' : ααSet α} (h : ∀ (a b : α), Ixx a b Ixx' a b) [h' : Filter.TendstoIxxClass Ixx' l₁ l₂] :
theorem Filter.HasBasis.tendstoIxxClass {α : Type u_1} {ι : Type u_3} {p : ιProp} {s : ιSet α} {l : } (hl : ) {Ixx : ααSet α} (H : ∀ (i : ι), p i∀ (x : α), x s i∀ (y : α), y s iIxx x y s i) :
instance Filter.tendsto_Icc_atTop_atTop {α : Type u_1} [] :
Filter.TendstoIxxClass Set.Icc Filter.atTop Filter.atTop
instance Filter.tendsto_Ico_atTop_atTop {α : Type u_1} [] :
Filter.TendstoIxxClass Set.Ico Filter.atTop Filter.atTop
instance Filter.tendsto_Ioc_atTop_atTop {α : Type u_1} [] :
Filter.TendstoIxxClass Set.Ioc Filter.atTop Filter.atTop
instance Filter.tendsto_Ioo_atTop_atTop {α : Type u_1} [] :
Filter.TendstoIxxClass Set.Ioo Filter.atTop Filter.atTop
instance Filter.tendsto_Icc_atBot_atBot {α : Type u_1} [] :
Filter.TendstoIxxClass Set.Icc Filter.atBot Filter.atBot
instance Filter.tendsto_Ico_atBot_atBot {α : Type u_1} [] :
Filter.TendstoIxxClass Set.Ico Filter.atBot Filter.atBot
instance Filter.tendsto_Ioc_atBot_atBot {α : Type u_1} [] :
Filter.TendstoIxxClass Set.Ioc Filter.atBot Filter.atBot
instance Filter.tendsto_Ioo_atBot_atBot {α : Type u_1} [] :
Filter.TendstoIxxClass Set.Ioo Filter.atBot Filter.atBot
instance Filter.OrdConnected.tendsto_Icc {α : Type u_1} [] {s : Set α} [hs : ] :
instance Filter.tendsto_Ico_Ici_Ici {α : Type u_1} [] {a : α} :
instance Filter.tendsto_Ico_Ioi_Ioi {α : Type u_1} [] {a : α} :
instance Filter.tendsto_Ico_Iic_Iio {α : Type u_1} [] {a : α} :
instance Filter.tendsto_Ico_Iio_Iio {α : Type u_1} [] {a : α} :
instance Filter.tendsto_Ioc_Ici_Ioi {α : Type u_1} [] {a : α} :
instance Filter.tendsto_Ioc_Iic_Iic {α : Type u_1} [] {a : α} :
instance Filter.tendsto_Ioc_Iio_Iio {α : Type u_1} [] {a : α} :
instance Filter.tendsto_Ioc_Ioi_Ioi {α : Type u_1} [] {a : α} :
instance Filter.tendsto_Ioo_Ici_Ioi {α : Type u_1} [] {a : α} :
instance Filter.tendsto_Ioo_Iic_Iio {α : Type u_1} [] {a : α} :
instance Filter.tendsto_Ioo_Ioi_Ioi {α : Type u_1} [] {a : α} :
instance Filter.tendsto_Ioo_Iio_Iio {α : Type u_1} [] {a : α} :
instance Filter.tendsto_Icc_Icc_Icc {α : Type u_1} [] {a : α} {b : α} :
instance Filter.tendsto_Ioc_Icc_Icc {α : Type u_1} [] {a : α} {b : α} :
instance Filter.tendsto_Icc_pure_pure {α : Type u_1} [] {a : α} :
instance Filter.tendsto_Ico_pure_bot {α : Type u_1} [] {a : α} :
instance Filter.tendsto_Ioc_pure_bot {α : Type u_1} [] {a : α} :
instance Filter.tendsto_Ioo_pure_bot {α : Type u_1} [] {a : α} :
instance Filter.tendsto_Icc_uIcc_uIcc {α : Type u_1} [] {a : α} {b : α} :
instance Filter.tendsto_Ioc_uIcc_uIcc {α : Type u_1} [] {a : α} {b : α} :
instance Filter.tendsto_uIcc_of_Icc {α : Type u_1} [] {l : } [Filter.TendstoIxxClass Set.Icc l l] :
theorem Filter.Tendsto.uIcc {α : Type u_1} {β : Type u_2} [] {l : } [Filter.TendstoIxxClass Set.Icc l l] {f : βα} {g : βα} {lb : } (hf : Filter.Tendsto f lb l) (hg : Filter.Tendsto g lb l) :
Filter.Tendsto (fun x => Set.uIcc (f x) (g x)) lb ()