Documentation

Mathlib.Order.Filter.Partial

Tendsto for relations and partial functions #

This file generalizes Filter definitions from functions to partial functions and relations.

Considering functions and partial functions as relations #

A function f : α → β can be considered as the relation Rel α β which relates x and f x for all x, and nothing else. This relation is called Function.Graph f.

A partial function f : α →. β can be considered as the relation Rel α β which relates x and f x for all x for which f x exists, and nothing else. This relation is called PFun.Graph' f.

In this regard, a function is a relation for which every element in α is related to exactly one element in β and a partial function is a relation for which every element in α is related to at most one element in β.

This file leverages this analogy to generalize Filter definitions from functions to partial functions and relations.

Notes #

Set.preimage can be generalized to relations in two ways:

We first take care of relations. Then the definitions for partial functions are taken as special cases of the definitions for relations.

Relations #

def Filter.rmap {α : Type u} {β : Type v} (r : Rel α β) (l : Filter α) :

The forward map of a filter under a relation. Generalization of Filter.map to relations. Note that Rel.core generalizes Set.preimage.

Equations
theorem Filter.rmap_sets {α : Type u} {β : Type v} (r : Rel α β) (l : Filter α) :
@[simp]
theorem Filter.mem_rmap {α : Type u} {β : Type v} (r : Rel α β) (l : Filter α) (s : Set β) :
s rmap r l r.core s l
@[simp]
theorem Filter.rmap_rmap {α : Type u} {β : Type v} {γ : Type w} (r : Rel α β) (s : Rel β γ) (l : Filter α) :
rmap s (rmap r l) = rmap (r.comp s) l
@[simp]
theorem Filter.rmap_compose {α : Type u} {β : Type v} {γ : Type w} (r : Rel α β) (s : Rel β γ) :
rmap s rmap r = rmap (r.comp s)
def Filter.RTendsto {α : Type u} {β : Type v} (r : Rel α β) (l₁ : Filter α) (l₂ : Filter β) :

Generic "limit of a relation" predicate. RTendsto r l₁ l₂ asserts that for every l₂-neighborhood a, the r-core of a is an l₁-neighborhood. One generalization of Filter.Tendsto to relations.

Equations
theorem Filter.rtendsto_def {α : Type u} {β : Type v} (r : Rel α β) (l₁ : Filter α) (l₂ : Filter β) :
RTendsto r l₁ l₂ sl₂, r.core s l₁
def Filter.rcomap {α : Type u} {β : Type v} (r : Rel α β) (f : Filter β) :

One way of taking the inverse map of a filter under a relation. One generalization of Filter.comap to relations. Note that Rel.core generalizes Set.preimage.

Equations
theorem Filter.rcomap_sets {α : Type u} {β : Type v} (r : Rel α β) (f : Filter β) :
(rcomap r f).sets = Rel.image (fun (s : Set β) (t : Set α) => r.core s t) f.sets
theorem Filter.rcomap_rcomap {α : Type u} {β : Type v} {γ : Type w} (r : Rel α β) (s : Rel β γ) (l : Filter γ) :
rcomap r (rcomap s l) = rcomap (r.comp s) l
@[simp]
theorem Filter.rcomap_compose {α : Type u} {β : Type v} {γ : Type w} (r : Rel α β) (s : Rel β γ) :
theorem Filter.rtendsto_iff_le_rcomap {α : Type u} {β : Type v} (r : Rel α β) (l₁ : Filter α) (l₂ : Filter β) :
RTendsto r l₁ l₂ l₁ rcomap r l₂
def Filter.rcomap' {α : Type u} {β : Type v} (r : Rel α β) (f : Filter β) :

One way of taking the inverse map of a filter under a relation. Generalization of Filter.comap to relations.

Equations
@[simp]
theorem Filter.mem_rcomap' {α : Type u} {β : Type v} (r : Rel α β) (l : Filter β) (s : Set α) :
s rcomap' r l tl, r.preimage t s
theorem Filter.rcomap'_sets {α : Type u} {β : Type v} (r : Rel α β) (f : Filter β) :
(rcomap' r f).sets = Rel.image (fun (s : Set β) (t : Set α) => r.preimage s t) f.sets
@[simp]
theorem Filter.rcomap'_rcomap' {α : Type u} {β : Type v} {γ : Type w} (r : Rel α β) (s : Rel β γ) (l : Filter γ) :
rcomap' r (rcomap' s l) = rcomap' (r.comp s) l
@[simp]
theorem Filter.rcomap'_compose {α : Type u} {β : Type v} {γ : Type w} (r : Rel α β) (s : Rel β γ) :
def Filter.RTendsto' {α : Type u} {β : Type v} (r : Rel α β) (l₁ : Filter α) (l₂ : Filter β) :

Generic "limit of a relation" predicate. RTendsto' r l₁ l₂ asserts that for every l₂-neighborhood a, the r-preimage of a is an l₁-neighborhood. One generalization of Filter.Tendsto to relations.

Equations
theorem Filter.rtendsto'_def {α : Type u} {β : Type v} (r : Rel α β) (l₁ : Filter α) (l₂ : Filter β) :
RTendsto' r l₁ l₂ sl₂, r.preimage s l₁
theorem Filter.tendsto_iff_rtendsto {α : Type u} {β : Type v} (l₁ : Filter α) (l₂ : Filter β) (f : αβ) :
Tendsto f l₁ l₂ RTendsto (Function.graph f) l₁ l₂
theorem Filter.tendsto_iff_rtendsto' {α : Type u} {β : Type v} (l₁ : Filter α) (l₂ : Filter β) (f : αβ) :
Tendsto f l₁ l₂ RTendsto' (Function.graph f) l₁ l₂

Partial functions #

def Filter.pmap {α : Type u} {β : Type v} (f : α →. β) (l : Filter α) :

The forward map of a filter under a partial function. Generalization of Filter.map to partial functions.

Equations
@[simp]
theorem Filter.mem_pmap {α : Type u} {β : Type v} (f : α →. β) (l : Filter α) (s : Set β) :
s pmap f l f.core s l
def Filter.PTendsto {α : Type u} {β : Type v} (f : α →. β) (l₁ : Filter α) (l₂ : Filter β) :

Generic "limit of a partial function" predicate. PTendsto r l₁ l₂ asserts that for every l₂-neighborhood a, the p-core of a is an l₁-neighborhood. One generalization of Filter.Tendsto to partial function.

Equations
theorem Filter.ptendsto_def {α : Type u} {β : Type v} (f : α →. β) (l₁ : Filter α) (l₂ : Filter β) :
PTendsto f l₁ l₂ sl₂, f.core s l₁
theorem Filter.ptendsto_iff_rtendsto {α : Type u} {β : Type v} (l₁ : Filter α) (l₂ : Filter β) (f : α →. β) :
PTendsto f l₁ l₂ RTendsto f.graph' l₁ l₂
theorem Filter.pmap_res {α : Type u} {β : Type v} (l : Filter α) (s : Set α) (f : αβ) :
pmap (PFun.res f s) l = map f (lprincipal s)
theorem Filter.tendsto_iff_ptendsto {α : Type u} {β : Type v} (l₁ : Filter α) (l₂ : Filter β) (s : Set α) (f : αβ) :
Tendsto f (l₁principal s) l₂ PTendsto (PFun.res f s) l₁ l₂
theorem Filter.tendsto_iff_ptendsto_univ {α : Type u} {β : Type v} (l₁ : Filter α) (l₂ : Filter β) (f : αβ) :
Tendsto f l₁ l₂ PTendsto (PFun.res f Set.univ) l₁ l₂
def Filter.pcomap' {α : Type u} {β : Type v} (f : α →. β) (l : Filter β) :

Inverse map of a filter under a partial function. One generalization of Filter.comap to partial functions.

Equations
def Filter.PTendsto' {α : Type u} {β : Type v} (f : α →. β) (l₁ : Filter α) (l₂ : Filter β) :

Generic "limit of a partial function" predicate. PTendsto' r l₁ l₂ asserts that for every l₂-neighborhood a, the p-preimage of a is an l₁-neighborhood. One generalization of Filter.Tendsto to partial functions.

Equations
theorem Filter.ptendsto'_def {α : Type u} {β : Type v} (f : α →. β) (l₁ : Filter α) (l₂ : Filter β) :
PTendsto' f l₁ l₂ sl₂, f.preimage s l₁
theorem Filter.ptendsto_of_ptendsto' {α : Type u} {β : Type v} {f : α →. β} {l₁ : Filter α} {l₂ : Filter β} :
PTendsto' f l₁ l₂PTendsto f l₁ l₂
theorem Filter.ptendsto'_of_ptendsto {α : Type u} {β : Type v} {f : α →. β} {l₁ : Filter α} {l₂ : Filter β} (h : f.Dom l₁) :
PTendsto f l₁ l₂PTendsto' f l₁ l₂