mathlib3 documentation

order.filter.interval

Convergence of intervals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

If both a and b tend to some filter l₁, sometimes this implies that Ixx a b tends to l₂.small_sets, 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₂.small_sets 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 of this typeclass
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₂.small_sets
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₂.small_sets
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₂.small_sets
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₂.small_sets
theorem filter.tendsto_Ixx_class_principal {α : Type u_1} [preorder α] {s t : set α} {Ixx : α α set α} :
filter.tendsto_Ixx_class Ixx (filter.principal s) (filter.principal t) (x : α), x s (y : α), y s Ixx 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 i Ixx x y s i) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem filter.tendsto.uIcc {α : 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 : β), set.uIcc (f x) (g x)) lb l.small_sets