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

tendsto_Ixx : filter.tendsto (λ (p : α × α), Ixx p.fst p.snd) (l₁ ×ᶠ l₁) (filter.lift' l₂ set.powerset)

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 ∈ 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₂] :

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) :

filter.tendsto_Ixx_class Ixx l l

@[protected, instance]

def filter.tendsto_Icc_at_top_at_top {α : Type u_1} [preorder α] :

filter.tendsto_Ixx_class set.Icc filter.at_top filter.at_top

@[protected, instance]

def filter.tendsto_Ico_at_top_at_top {α : Type u_1} [preorder α] :

filter.tendsto_Ixx_class set.Ico filter.at_top filter.at_top

@[protected, instance]

def filter.tendsto_Ioc_at_top_at_top {α : Type u_1} [preorder α] :

filter.tendsto_Ixx_class set.Ioc filter.at_top filter.at_top

@[protected, instance]

def filter.tendsto_Ioo_at_top_at_top {α : Type u_1} [preorder α] :

filter.tendsto_Ixx_class set.Ioo filter.at_top filter.at_top

@[protected, instance]

def filter.tendsto_Icc_at_bot_at_bot {α : Type u_1} [preorder α] :

filter.tendsto_Ixx_class set.Icc filter.at_bot filter.at_bot

@[protected, instance]

def filter.tendsto_Ico_at_bot_at_bot {α : Type u_1} [preorder α] :

filter.tendsto_Ixx_class set.Ico filter.at_bot filter.at_bot

@[protected, instance]

def filter.tendsto_Ioc_at_bot_at_bot {α : Type u_1} [preorder α] :

filter.tendsto_Ixx_class set.Ioc filter.at_bot filter.at_bot

@[protected, instance]

def filter.tendsto_Ioo_at_bot_at_bot {α : Type u_1} [preorder α] :

filter.tendsto_Ixx_class set.Ioo filter.at_bot filter.at_bot

@[protected, instance]

def filter.ord_connected.tendsto_Icc {α : Type u_1} [preorder α] {s : set α} [hs : s.ord_connected] :

filter.tendsto_Ixx_class set.Icc (𝓟 s) (𝓟 s)

@[protected, instance]

def filter.tendsto_Ico_Ici_Ici {α : Type u_1} [preorder α] {a : α} :

filter.tendsto_Ixx_class set.Ico (𝓟 (set.Ici a)) (𝓟 (set.Ici a))

@[protected, instance]

def filter.tendsto_Ico_Ioi_Ioi {α : Type u_1} [preorder α] {a : α} :

filter.tendsto_Ixx_class set.Ico (𝓟 (set.Ioi a)) (𝓟 (set.Ioi a))

@[protected, instance]

def filter.tendsto_Ico_Iic_Iio {α : Type u_1} [preorder α] {a : α} :

filter.tendsto_Ixx_class set.Ico (𝓟 (set.Iic a)) (𝓟 (set.Iio a))

@[protected, instance]

def filter.tendsto_Ico_Iio_Iio {α : Type u_1} [preorder α] {a : α} :

filter.tendsto_Ixx_class set.Ico (𝓟 (set.Iio a)) (𝓟 (set.Iio a))

@[protected, instance]

def filter.tendsto_Ioc_Ici_Ioi {α : Type u_1} [preorder α] {a : α} :

filter.tendsto_Ixx_class set.Ioc (𝓟 (set.Ici a)) (𝓟 (set.Ioi a))

@[protected, instance]

def filter.tendsto_Ioc_Iic_Iic {α : Type u_1} [preorder α] {a : α} :

filter.tendsto_Ixx_class set.Ioc (𝓟 (set.Iic a)) (𝓟 (set.Iic a))

@[protected, instance]

def filter.tendsto_Ioc_Iio_Iio {α : Type u_1} [preorder α] {a : α} :

filter.tendsto_Ixx_class set.Ioc (𝓟 (set.Iio a)) (𝓟 (set.Iio a))

@[protected, instance]

def filter.tendsto_Ioc_Ioi_Ioi {α : Type u_1} [preorder α] {a : α} :

filter.tendsto_Ixx_class set.Ioc (𝓟 (set.Ioi a)) (𝓟 (set.Ioi a))

@[protected, instance]

def filter.tendsto_Ioo_Ici_Ioi {α : Type u_1} [preorder α] {a : α} :

filter.tendsto_Ixx_class set.Ioo (𝓟 (set.Ici a)) (𝓟 (set.Ioi a))

@[protected, instance]

def filter.tendsto_Ioo_Iic_Iio {α : Type u_1} [preorder α] {a : α} :

filter.tendsto_Ixx_class set.Ioo (𝓟 (set.Iic a)) (𝓟 (set.Iio a))

@[protected, instance]

def filter.tendsto_Ioo_Ioi_Ioi {α : Type u_1} [preorder α] {a : α} :

filter.tendsto_Ixx_class set.Ioo (𝓟 (set.Ioi a)) (𝓟 (set.Ioi a))

@[protected, instance]

def filter.tendsto_Ioo_Iio_Iio {α : Type u_1} [preorder α] {a : α} :

filter.tendsto_Ixx_class set.Ioo (𝓟 (set.Iio a)) (𝓟 (set.Iio a))

@[protected, instance]

def filter.tendsto_Icc_Icc_Icc {α : Type u_1} [preorder α] {a b : α} :

filter.tendsto_Ixx_class set.Icc (𝓟 (set.Icc a b)) (𝓟 (set.Icc a b))

@[protected, instance]

def filter.tendsto_Ioc_Icc_Icc {α : Type u_1} [preorder α] {a b : α} :

filter.tendsto_Ixx_class set.Ioc (𝓟 (set.Icc a b)) (𝓟 (set.Icc a b))

@[protected, instance]

def filter.tendsto_Icc_pure_pure {α : Type u_1} [partial_order α] {a : α} :

filter.tendsto_Ixx_class set.Icc (pure a) (pure a)

@[protected, instance]

def filter.tendsto_Ico_pure_bot {α : Type u_1} [partial_order α] {a : α} :

filter.tendsto_Ixx_class set.Ico (pure a) ⊥

@[protected, instance]

def filter.tendsto_Ioc_pure_bot {α : Type u_1} [partial_order α] {a : α} :

filter.tendsto_Ixx_class set.Ioc (pure a) ⊥

@[protected, instance]

def filter.tendsto_Ioo_pure_bot {α : Type u_1} [partial_order α] {a : α} :

filter.tendsto_Ixx_class set.Ioo (pure a) ⊥

@[protected, instance]

def filter.tendsto_Icc_interval_interval {α : Type u_1} [linear_order α] {a b : α} :

filter.tendsto_Ixx_class set.Icc (𝓟 [a, b]) (𝓟 [a, b])

@[protected, instance]

def filter.tendsto_Ioc_interval_interval {α : Type u_1} [linear_order α] {a b : α} :

filter.tendsto_Ixx_class set.Ioc (𝓟 [a, b]) (𝓟 [a, b])

@[protected, instance]

def filter.tendsto_interval_of_Icc {α : Type u_1} [linear_order α] {l : filter α} [filter.tendsto_Ixx_class set.Icc l l] :

filter.tendsto_Ixx_class set.interval l l

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)