mathlib documentation

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₂.lift' powerset, i.e., for any s ∈ l₂ eventually Ixx a b becomes a subset of s. Here and below Ixx is one of Icc, Ico, Ioc, and Ioo. We define filter.tendsto_Ixx_class 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 tendsto_Ixx_class Ico (𝓟 $ Iic a) (𝓟 $ Iio a), i.e., if u₁ n and u₂ n belong eventually to Iic a, then the interval Ico (u₁ n) (u₂ n) is eventually included in Iio a.

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

Input filter Ixx = Icc Ixx = Ico Ixx = Ioc Ixx = Ioo
at_top at_top at_top at_top at_top
at_bot at_bot at_bot at_bot at_bot
pure a pure a
𝓟 (Iic a) 𝓟 (Iic a) 𝓟 (Iio a) 𝓟 (Iic a) 𝓟 (Iio a)
𝓟 (Ici a) 𝓟 (Ici a) 𝓟 (Ici a) 𝓟 (Ioi a) 𝓟 (Ioi a)
𝓟 (Ioi a) 𝓟 (Ioi a) 𝓟 (Ioi a) 𝓟 (Ioi a) 𝓟 (Ioi a)
𝓟 (Iio a) 𝓟 (Iio a) 𝓟 (Iio a) 𝓟 (Iio a) 𝓟 (Iio a)
𝓝 a 𝓝 a 𝓝 a 𝓝 a 𝓝 a
𝓝[Iic a] b 𝓝[Iic a] b 𝓝[Iio a] b 𝓝[Iic a] b 𝓝[Iio a] b
𝓝[Ici a] b 𝓝[Ici a] b 𝓝[Ici a] b 𝓝[Ioi a] b 𝓝[Ioi a] b
𝓝[Ioi a] b 𝓝[Ioi a] b 𝓝[Ioi a] b 𝓝[Ioi a] b 𝓝[Ioi a] b
𝓝[Iio a] b 𝓝[Iio a] b 𝓝[Iio a] b 𝓝[Iio a] b 𝓝[Iio a] b
@[class]
structure filter.tendsto_Ixx_class {α : Type u_1} [preorder α] (Ixx : α → α → set α) (l₁ : filter α) (l₂ : out_param (filter α)) :
Prop

A pair of filters l₁, l₂ has tendsto_Ixx_class Ixx property if Ixx a b tends to l₂.lift' powerset as a and b tend to l₁. In all instances Ixx is one of Icc, Ico, Ioc, or 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 tendsto_Ixx_class Ico (𝓟 $ Iic a) (𝓟 $ Iio a), i.e., if u₁ n and u₂ n belong eventually to Iic a, then the interval Ico (u₁ n) (u₂ n) is eventually included in Iio a.

We mark l₂ as an out_param 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₁ l₂ : filter α} [filter.tendsto_Ixx_class set.Icc l₁ l₂] {lb : filter β} {u₁ u₂ : β → α} (h₁ : filter.tendsto u₁ lb l₁) (h₂ : filter.tendsto u₂ lb l₁) :
filter.tendsto (λ (x : β), set.Icc (u₁ x) (u₂ x)) lb (l₂.lift' set.powerset)
theorem filter.tendsto.Ioc {α : Type u_1} {β : Type u_2} [preorder α] {l₁ l₂ : filter α} [filter.tendsto_Ixx_class set.Ioc l₁ l₂] {lb : filter β} {u₁ u₂ : β → α} (h₁ : filter.tendsto u₁ lb l₁) (h₂ : filter.tendsto u₂ lb l₁) :
filter.tendsto (λ (x : β), set.Ioc (u₁ x) (u₂ x)) lb (l₂.lift' set.powerset)
theorem filter.tendsto.Ico {α : Type u_1} {β : Type u_2} [preorder α] {l₁ l₂ : filter α} [filter.tendsto_Ixx_class set.Ico l₁ l₂] {lb : filter β} {u₁ u₂ : β → α} (h₁ : filter.tendsto u₁ lb l₁) (h₂ : filter.tendsto u₂ lb l₁) :
filter.tendsto (λ (x : β), set.Ico (u₁ x) (u₂ x)) lb (l₂.lift' set.powerset)
theorem filter.tendsto.Ioo {α : Type u_1} {β : Type u_2} [preorder α] {l₁ l₂ : filter α} [filter.tendsto_Ixx_class set.Ioo l₁ l₂] {lb : filter β} {u₁ u₂ : β → α} (h₁ : filter.tendsto u₁ lb l₁) (h₂ : filter.tendsto u₂ lb l₁) :
filter.tendsto (λ (x : β), set.Ioo (u₁ x) (u₂ x)) lb (l₂.lift' set.powerset)
theorem filter.tendsto_Ixx_class_principal {α : Type u_1} [preorder α] {s t : set α} {Ixx : α → α → set α} :
filter.tendsto_Ixx_class Ixx (𝓟 s) (𝓟 t) ∀ (x : α), x s∀ (y : α), y sIxx x y t
theorem filter.tendsto_Ixx_class_inf {α : Type u_1} [preorder α] {l₁ l₁' l₂ l₂' : filter α} {Ixx : α → α → set α} [h : filter.tendsto_Ixx_class Ixx l₁ l₂] [h' : filter.tendsto_Ixx_class Ixx l₁' l₂'] :
filter.tendsto_Ixx_class Ixx (l₁ l₁') (l₂ l₂')
theorem filter.tendsto_Ixx_class_of_subset {α : Type u_1} [preorder α] {l₁ l₂ : filter α} {Ixx Ixx' : α → α → set α} (h : ∀ (a b : α), Ixx a b Ixx' a b) [h' : filter.tendsto_Ixx_class Ixx' l₁ l₂] :
theorem filter.has_basis.tendsto_Ixx_class {α : Type u_1} [preorder α] {ι : Type u_2} {p : ι → Prop} {s : ι → set α} {l : filter α} (hl : l.has_basis p s) {Ixx : α → α → set α} (H : ∀ (i : ι), p i∀ (x : α), x s i∀ (y : α), y s iIxx x y s i) :
@[protected, instance]
@[protected, instance]
def filter.tendsto_Ico_Ici_Ici {α : Type u_1} [preorder α] {a : α} :
@[protected, instance]
def filter.tendsto_Ico_Ioi_Ioi {α : Type u_1} [preorder α] {a : α} :
@[protected, instance]
def filter.tendsto_Ico_Iic_Iio {α : Type u_1} [preorder α] {a : α} :
@[protected, instance]
def filter.tendsto_Ico_Iio_Iio {α : Type u_1} [preorder α] {a : α} :
@[protected, instance]
def filter.tendsto_Ioc_Ici_Ioi {α : Type u_1} [preorder α] {a : α} :
@[protected, instance]
def filter.tendsto_Ioc_Iic_Iic {α : Type u_1} [preorder α] {a : α} :
@[protected, instance]
def filter.tendsto_Ioc_Iio_Iio {α : Type u_1} [preorder α] {a : α} :
@[protected, instance]
def filter.tendsto_Ioc_Ioi_Ioi {α : Type u_1} [preorder α] {a : α} :
@[protected, instance]
def filter.tendsto_Ioo_Ici_Ioi {α : Type u_1} [preorder α] {a : α} :
@[protected, instance]
def filter.tendsto_Ioo_Iic_Iio {α : Type u_1} [preorder α] {a : α} :
@[protected, instance]
def filter.tendsto_Ioo_Ioi_Ioi {α : Type u_1} [preorder α] {a : α} :
@[protected, instance]
def filter.tendsto_Ioo_Iio_Iio {α : Type u_1} [preorder α] {a : α} :
@[protected, instance]
def filter.tendsto_Icc_Icc_Icc {α : Type u_1} [preorder α] {a b : α} :
@[protected, instance]
def filter.tendsto_Ioc_Icc_Icc {α : Type u_1} [preorder α] {a b : α} :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem filter.tendsto.interval {α : Type u_1} {β : Type u_2} [linear_order α] {l : filter α} [filter.tendsto_Ixx_class set.Icc l l] {f g : β → α} {lb : filter β} (hf : filter.tendsto f lb l) (hg : filter.tendsto g lb l) :
filter.tendsto (λ (x : β), [f x, g x]) lb (l.lift' set.powerset)