# mathlibdocumentation

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₂.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 α} [ l₂] {lb : filter β} {u₁ u₂ : β → α} (h₁ : lb l₁) (h₂ : 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 α} [ l₂] {lb : filter β} {u₁ u₂ : β → α} (h₁ : lb l₁) (h₂ : 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 α} [ l₂] {lb : filter β} {u₁ u₂ : β → α} (h₁ : lb l₁) (h₂ : 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 α} [ l₂] {lb : filter β} {u₁ u₂ : β → α} (h₁ : lb l₁) (h₂ : 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 α} :
∀ (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 : l₁ l₂] [h' : l₁' l₂'] :
(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' : l₁ l₂] :
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) :
l
@[protected, instance]
def filter.tendsto_Icc_at_top_at_top {α : Type u_1} [preorder α] :
@[protected, instance]
def filter.tendsto_Ico_at_top_at_top {α : Type u_1} [preorder α] :
@[protected, instance]
def filter.tendsto_Ioc_at_top_at_top {α : Type u_1} [preorder α] :
@[protected, instance]
def filter.tendsto_Ioo_at_top_at_top {α : Type u_1} [preorder α] :
@[protected, instance]
def filter.tendsto_Icc_at_bot_at_bot {α : Type u_1} [preorder α] :
@[protected, instance]
def filter.tendsto_Ico_at_bot_at_bot {α : Type u_1} [preorder α] :
@[protected, instance]
def filter.tendsto_Ioc_at_bot_at_bot {α : Type u_1} [preorder α] :
@[protected, instance]
def filter.tendsto_Ioo_at_bot_at_bot {α : Type u_1} [preorder α] :
@[protected, instance]
def filter.ord_connected.tendsto_Icc {α : Type u_1} [preorder α] {s : set α} [hs : s.ord_connected] :
@[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]
def filter.tendsto_Icc_pure_pure {α : Type u_1} {a : α} :
@[protected, instance]
def filter.tendsto_Ico_pure_bot {α : Type u_1} {a : α} :
@[protected, instance]
def filter.tendsto_Ioc_pure_bot {α : Type u_1} {a : α} :
@[protected, instance]
def filter.tendsto_Ioo_pure_bot {α : Type u_1} {a : α} :
@[protected, instance]
def filter.tendsto_Icc_interval_interval {α : Type u_1} [linear_order α] {a b : α} :
@[protected, instance]
def filter.tendsto_Ioc_interval_interval {α : Type u_1} [linear_order α] {a b : α} :
@[protected, instance]
def filter.tendsto_interval_of_Icc {α : Type u_1} [linear_order α] {l : filter α}  :
theorem filter.tendsto.interval {α : Type u_1} {β : Type u_2} [linear_order α] {l : filter α} {f g : β → α} {lb : filter β} (hf : lb l) (hg : lb l) :
filter.tendsto (λ (x : β), set.interval (f x) (g x)) lb l.small_sets