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₁ : Filter α) (l₂ : outParam (Filter α)) :

tendsto_Ixx : Filter.Tendsto (fun p => Ixx p.fst p.snd) (l₁ ×ˢ l₁) (Filter.smallSets 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} [Preorder α] {l₁ : Filter α} {l₂ : Filter α} [Filter.TendstoIxxClass Set.Icc l₁ l₂] {lb : Filter β} {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 (Filter.smallSets l₂)

theorem Filter.Tendsto.Ioc {α : Type u_1} {β : Type u_2} [Preorder α] {l₁ : Filter α} {l₂ : Filter α} [Filter.TendstoIxxClass Set.Ioc l₁ l₂] {lb : Filter β} {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 (Filter.smallSets l₂)

theorem Filter.Tendsto.Ico {α : Type u_1} {β : Type u_2} [Preorder α] {l₁ : Filter α} {l₂ : Filter α} [Filter.TendstoIxxClass Set.Ico l₁ l₂] {lb : Filter β} {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 (Filter.smallSets l₂)

theorem Filter.Tendsto.Ioo {α : Type u_1} {β : Type u_2} [Preorder α] {l₁ : Filter α} {l₂ : Filter α} [Filter.TendstoIxxClass Set.Ioo l₁ l₂] {lb : Filter β} {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 (Filter.smallSets l₂)

theorem Filter.tendstoIxxClass_principal {α : Type u_1} {s : Set α} {t : Set α} {Ixx : α → α → Set α} :

Filter.TendstoIxxClass Ixx (Filter.principal s) (Filter.principal t) ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → Ixx x y ⊆ t

theorem Filter.tendstoIxxClass_inf {α : Type u_1} {l₁ : Filter α} {l₁' : Filter α} {l₂ : Filter α} {l₂' : Filter α} {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₁ : Filter α} {l₂ : Filter α} {Ixx : α → α → Set α} {Ixx' : α → α → Set α} (h : ∀ (a b : α), Ixx a b ⊆ Ixx' a b) [h' : Filter.TendstoIxxClass Ixx' l₁ l₂] :

Filter.TendstoIxxClass Ixx l₁ l₂

theorem Filter.HasBasis.tendstoIxxClass {α : Type u_1} {ι : Type u_3} {p : ι → Prop} {s : ι → Set α} {l : Filter α} (hl : Filter.HasBasis l p s) {Ixx : α → α → Set α} (H : ∀ (i : ι), p i → ∀ (x : α), x ∈ s i → ∀ (y : α), y ∈ s i → Ixx x y ⊆ s i) :

Filter.TendstoIxxClass Ixx l l

instance Filter.tendsto_Icc_atTop_atTop {α : Type u_1} [Preorder α] :

Filter.TendstoIxxClass Set.Icc Filter.atTop Filter.atTop

Equations

@Filter.tendsto_Icc_atTop_atTop = @Filter.tendsto_Icc_atTop_atTop.proof_1

instance Filter.tendsto_Ico_atTop_atTop {α : Type u_1} [Preorder α] :

Filter.TendstoIxxClass Set.Ico Filter.atTop Filter.atTop

Equations

@Filter.tendsto_Ico_atTop_atTop = @Filter.tendsto_Ico_atTop_atTop.proof_1

instance Filter.tendsto_Ioc_atTop_atTop {α : Type u_1} [Preorder α] :

Filter.TendstoIxxClass Set.Ioc Filter.atTop Filter.atTop

Equations

@Filter.tendsto_Ioc_atTop_atTop = @Filter.tendsto_Ioc_atTop_atTop.proof_1

instance Filter.tendsto_Ioo_atTop_atTop {α : Type u_1} [Preorder α] :

Filter.TendstoIxxClass Set.Ioo Filter.atTop Filter.atTop

Equations

@Filter.tendsto_Ioo_atTop_atTop = @Filter.tendsto_Ioo_atTop_atTop.proof_1

instance Filter.tendsto_Icc_atBot_atBot {α : Type u_1} [Preorder α] :

Filter.TendstoIxxClass Set.Icc Filter.atBot Filter.atBot

Equations

@Filter.tendsto_Icc_atBot_atBot = @Filter.tendsto_Icc_atBot_atBot.proof_1

instance Filter.tendsto_Ico_atBot_atBot {α : Type u_1} [Preorder α] :

Filter.TendstoIxxClass Set.Ico Filter.atBot Filter.atBot

Equations

@Filter.tendsto_Ico_atBot_atBot = @Filter.tendsto_Ico_atBot_atBot.proof_1

instance Filter.tendsto_Ioc_atBot_atBot {α : Type u_1} [Preorder α] :

Filter.TendstoIxxClass Set.Ioc Filter.atBot Filter.atBot

Equations

@Filter.tendsto_Ioc_atBot_atBot = @Filter.tendsto_Ioc_atBot_atBot.proof_1

instance Filter.tendsto_Ioo_atBot_atBot {α : Type u_1} [Preorder α] :

Filter.TendstoIxxClass Set.Ioo Filter.atBot Filter.atBot

Equations

@Filter.tendsto_Ioo_atBot_atBot = @Filter.tendsto_Ioo_atBot_atBot.proof_1

instance Filter.OrdConnected.tendsto_Icc {α : Type u_1} [Preorder α] {s : Set α} [hs : Set.OrdConnected s] :

Filter.TendstoIxxClass Set.Icc (Filter.principal s) (Filter.principal s)

Equations

@Filter.OrdConnected.tendsto_Icc = @Filter.OrdConnected.tendsto_Icc.proof_1

instance Filter.tendsto_Ico_Ici_Ici {α : Type u_1} [Preorder α] {a : α} :

Filter.TendstoIxxClass Set.Ico (Filter.principal (Set.Ici a)) (Filter.principal (Set.Ici a))

Equations

@Filter.tendsto_Ico_Ici_Ici = @Filter.tendsto_Ico_Ici_Ici.proof_1

instance Filter.tendsto_Ico_Ioi_Ioi {α : Type u_1} [Preorder α] {a : α} :

Filter.TendstoIxxClass Set.Ico (Filter.principal (Set.Ioi a)) (Filter.principal (Set.Ioi a))

Equations

@Filter.tendsto_Ico_Ioi_Ioi = @Filter.tendsto_Ico_Ioi_Ioi.proof_1

instance Filter.tendsto_Ico_Iic_Iio {α : Type u_1} [Preorder α] {a : α} :

Filter.TendstoIxxClass Set.Ico (Filter.principal (Set.Iic a)) (Filter.principal (Set.Iio a))

Equations

@Filter.tendsto_Ico_Iic_Iio = @Filter.tendsto_Ico_Iic_Iio.proof_1

instance Filter.tendsto_Ico_Iio_Iio {α : Type u_1} [Preorder α] {a : α} :

Filter.TendstoIxxClass Set.Ico (Filter.principal (Set.Iio a)) (Filter.principal (Set.Iio a))

Equations

@Filter.tendsto_Ico_Iio_Iio = @Filter.tendsto_Ico_Iio_Iio.proof_1

instance Filter.tendsto_Ioc_Ici_Ioi {α : Type u_1} [Preorder α] {a : α} :

Filter.TendstoIxxClass Set.Ioc (Filter.principal (Set.Ici a)) (Filter.principal (Set.Ioi a))

Equations

@Filter.tendsto_Ioc_Ici_Ioi = @Filter.tendsto_Ioc_Ici_Ioi.proof_1

instance Filter.tendsto_Ioc_Iic_Iic {α : Type u_1} [Preorder α] {a : α} :

Filter.TendstoIxxClass Set.Ioc (Filter.principal (Set.Iic a)) (Filter.principal (Set.Iic a))

Equations

@Filter.tendsto_Ioc_Iic_Iic = @Filter.tendsto_Ioc_Iic_Iic.proof_1

instance Filter.tendsto_Ioc_Iio_Iio {α : Type u_1} [Preorder α] {a : α} :

Filter.TendstoIxxClass Set.Ioc (Filter.principal (Set.Iio a)) (Filter.principal (Set.Iio a))

Equations

@Filter.tendsto_Ioc_Iio_Iio = @Filter.tendsto_Ioc_Iio_Iio.proof_1

instance Filter.tendsto_Ioc_Ioi_Ioi {α : Type u_1} [Preorder α] {a : α} :

Filter.TendstoIxxClass Set.Ioc (Filter.principal (Set.Ioi a)) (Filter.principal (Set.Ioi a))

Equations

@Filter.tendsto_Ioc_Ioi_Ioi = @Filter.tendsto_Ioc_Ioi_Ioi.proof_1

instance Filter.tendsto_Ioo_Ici_Ioi {α : Type u_1} [Preorder α] {a : α} :

Filter.TendstoIxxClass Set.Ioo (Filter.principal (Set.Ici a)) (Filter.principal (Set.Ioi a))

Equations

@Filter.tendsto_Ioo_Ici_Ioi = @Filter.tendsto_Ioo_Ici_Ioi.proof_1

instance Filter.tendsto_Ioo_Iic_Iio {α : Type u_1} [Preorder α] {a : α} :

Filter.TendstoIxxClass Set.Ioo (Filter.principal (Set.Iic a)) (Filter.principal (Set.Iio a))

Equations

@Filter.tendsto_Ioo_Iic_Iio = @Filter.tendsto_Ioo_Iic_Iio.proof_1

instance Filter.tendsto_Ioo_Ioi_Ioi {α : Type u_1} [Preorder α] {a : α} :

Filter.TendstoIxxClass Set.Ioo (Filter.principal (Set.Ioi a)) (Filter.principal (Set.Ioi a))

Equations

@Filter.tendsto_Ioo_Ioi_Ioi = @Filter.tendsto_Ioo_Ioi_Ioi.proof_1

instance Filter.tendsto_Ioo_Iio_Iio {α : Type u_1} [Preorder α] {a : α} :

Filter.TendstoIxxClass Set.Ioo (Filter.principal (Set.Iio a)) (Filter.principal (Set.Iio a))

Equations

@Filter.tendsto_Ioo_Iio_Iio = @Filter.tendsto_Ioo_Iio_Iio.proof_1

instance Filter.tendsto_Icc_Icc_Icc {α : Type u_1} [Preorder α] {a : α} {b : α} :

Filter.TendstoIxxClass Set.Icc (Filter.principal (Set.Icc a b)) (Filter.principal (Set.Icc a b))

Equations

@Filter.tendsto_Icc_Icc_Icc = @Filter.tendsto_Icc_Icc_Icc.proof_1

instance Filter.tendsto_Ioc_Icc_Icc {α : Type u_1} [Preorder α] {a : α} {b : α} :

Filter.TendstoIxxClass Set.Ioc (Filter.principal (Set.Icc a b)) (Filter.principal (Set.Icc a b))

Equations

@Filter.tendsto_Ioc_Icc_Icc = @Filter.tendsto_Ioc_Icc_Icc.proof_1

instance Filter.tendsto_Icc_pure_pure {α : Type u_1} [PartialOrder α] {a : α} :

Filter.TendstoIxxClass Set.Icc (pure a) (pure a)

Equations

@Filter.tendsto_Icc_pure_pure = @Filter.tendsto_Icc_pure_pure.proof_1

instance Filter.tendsto_Ico_pure_bot {α : Type u_1} [PartialOrder α] {a : α} :

Filter.TendstoIxxClass Set.Ico (pure a) ⊥

Equations

@Filter.tendsto_Ico_pure_bot = @Filter.tendsto_Ico_pure_bot.proof_1

instance Filter.tendsto_Ioc_pure_bot {α : Type u_1} [PartialOrder α] {a : α} :

Filter.TendstoIxxClass Set.Ioc (pure a) ⊥

Equations

@Filter.tendsto_Ioc_pure_bot = @Filter.tendsto_Ioc_pure_bot.proof_1

instance Filter.tendsto_Ioo_pure_bot {α : Type u_1} [PartialOrder α] {a : α} :

Filter.TendstoIxxClass Set.Ioo (pure a) ⊥

Equations

@Filter.tendsto_Ioo_pure_bot = @Filter.tendsto_Ioo_pure_bot.proof_1

instance Filter.tendsto_Icc_uIcc_uIcc {α : Type u_1} [LinearOrder α] {a : α} {b : α} :

Filter.TendstoIxxClass Set.Icc (Filter.principal (Set.uIcc a b)) (Filter.principal (Set.uIcc a b))

Equations

@Filter.tendsto_Icc_uIcc_uIcc = @Filter.tendsto_Icc_uIcc_uIcc.proof_1

instance Filter.tendsto_Ioc_uIcc_uIcc {α : Type u_1} [LinearOrder α] {a : α} {b : α} :

Filter.TendstoIxxClass Set.Ioc (Filter.principal (Set.uIcc a b)) (Filter.principal (Set.uIcc a b))

Equations

@Filter.tendsto_Ioc_uIcc_uIcc = @Filter.tendsto_Ioc_uIcc_uIcc.proof_1

instance Filter.tendsto_uIcc_of_Icc {α : Type u_1} [LinearOrder α] {l : Filter α} [Filter.TendstoIxxClass Set.Icc l l] :

Filter.TendstoIxxClass Set.uIcc l l

Equations

@Filter.tendsto_uIcc_of_Icc = @Filter.tendsto_uIcc_of_Icc.proof_1

theorem Filter.Tendsto.uIcc {α : Type u_1} {β : Type u_2} [LinearOrder α] {l : Filter α} [Filter.TendstoIxxClass Set.Icc l l] {f : β → α} {g : β → α} {lb : Filter β} (hf : Filter.Tendsto f lb l) (hg : Filter.Tendsto g lb l) :

Filter.Tendsto (fun x => Set.uIcc (f x) (g x)) lb (Filter.smallSets l)