mathlib3 documentation

order.filter.partial

tendsto for relations and partial functions #

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

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 filter.rmap r l r.core s l
@[simp]
theorem filter.rmap_rmap {α : Type u} {β : Type v} {γ : Type w} (r : rel α β) (s : rel β γ) (l : filter α) :
@[simp]
theorem filter.rmap_compose {α : Type u} {β : Type v} {γ : Type w} (r : rel α β) (s : rel β γ) :
def filter.rtendsto {α : Type u} {β : Type v} (r : rel α β) (l₁ : filter α) (l₂ : filter β) :
Prop

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 β) :
filter.rtendsto r l₁ l₂ (s : set β), s l₂ 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 β) :
(filter.rcomap r f).sets = rel.image (λ (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 γ) :
@[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 β) :
filter.rtendsto r l₁ l₂ l₁ filter.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 filter.rcomap' r l (t : set β) (H : t l), r.preimage t s
theorem filter.rcomap'_sets {α : Type u} {β : Type v} (r : rel α β) (f : filter β) :
(filter.rcomap' r f).sets = rel.image (λ (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 γ) :
@[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 β) :
Prop

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 β) :
filter.rtendsto' r l₁ l₂ (s : set β), s l₂ r.preimage s l₁
theorem filter.tendsto_iff_rtendsto {α : Type u} {β : Type v} (l₁ : filter α) (l₂ : filter β) (f : α β) :
theorem filter.tendsto_iff_rtendsto' {α : Type u} {β : Type v} (l₁ : filter α) (l₂ : filter β) (f : α β) :

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 filter.pmap f l f.core s l
def filter.ptendsto {α : Type u} {β : Type v} (f : α →. β) (l₁ : filter α) (l₂ : filter β) :
Prop

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 β) :
filter.ptendsto f l₁ l₂ (s : set β), s l₂ f.core s l₁
theorem filter.ptendsto_iff_rtendsto {α : Type u} {β : Type v} (l₁ : filter α) (l₂ : filter β) (f : α →. β) :
filter.ptendsto f l₁ l₂ filter.rtendsto f.graph' l₁ l₂
theorem filter.pmap_res {α : Type u} {β : Type v} (l : filter α) (s : set α) (f : α β) :
theorem filter.tendsto_iff_ptendsto {α : Type u} {β : Type v} (l₁ : filter α) (l₂ : filter β) (s : set α) (f : α β) :
theorem filter.tendsto_iff_ptendsto_univ {α : Type u} {β : Type v} (l₁ : filter α) (l₂ : filter β) (f : α β) :
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 β) :
Prop

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 β) :
filter.ptendsto' f l₁ l₂ (s : set β), s l₂ f.preimage s l₁
theorem filter.ptendsto_of_ptendsto' {α : Type u} {β : Type v} {f : α →. β} {l₁ : filter α} {l₂ : filter β} :
filter.ptendsto' f l₁ l₂ filter.ptendsto f l₁ l₂
theorem filter.ptendsto'_of_ptendsto {α : Type u} {β : Type v} {f : α →. β} {l₁ : filter α} {l₂ : filter β} (h : f.dom l₁) :
filter.ptendsto f l₁ l₂ filter.ptendsto' f l₁ l₂