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:

• Rel.preimage returns the image of the set under the inverse relation.
• Rel.core returns the set of elements that are only related to those in the set. Both generalizations are sensible in the context of filters, so Filter.comap and Filter.Tendsto get two generalizations each.

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 α) : Filter β

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

Equations

• Filter.rmap r l = { sets := {s : Set β | Rel.core r s ∈ l}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

theorem Filter.rmap_sets {α : Type u} {β : Type v} (r : Rel α β) (l : Filter α) : (Filter.rmap r l).sets = Rel.core r ⁻¹' l.sets

@[simp]

theorem Filter.mem_rmap {α : Type u} {β : Type v} (r : Rel α β) (l : Filter α) (s : Set β) : s ∈ Filter.rmap r l ↔ Rel.core r s ∈ l

@[simp]

theorem Filter.rmap_rmap {α : Type u} {β : Type v} {γ : Type w} (r : Rel α β) (s : Rel β γ) (l : Filter α) : Filter.rmap s (Filter.rmap r l) = Filter.rmap (Rel.comp r s) l

@[simp]

theorem Filter.rmap_compose {α : Type u} {β : Type v} {γ : Type w} (r : Rel α β) (s : Rel β γ) : Filter.rmap s ∘ Filter.rmap r = Filter.rmap (Rel.comp r s)

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

• Filter.RTendsto r l₁ l₂ = (Filter.rmap r l₁ ≤ l₂)

theorem Filter.rtendsto_def {α : Type u} {β : Type v} (r : Rel α β) (l₁ : Filter α) (l₂ : Filter β) : Filter.RTendsto r l₁ l₂ ↔ ∀ s ∈ l₂, Rel.core r s ∈ l₁

def Filter.rcomap {α : Type u} {β : Type v} (r : Rel α β) (f : Filter β) : 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

• Filter.rcomap r f = { sets := Rel.image (fun (s : Set β) (t : Set α) => Rel.core r s ⊆ t) f.sets, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

theorem Filter.rcomap_sets {α : Type u} {β : Type v} (r : Rel α β) (f : Filter β) : (Filter.rcomap r f).sets = Rel.image (fun (s : Set β) (t : Set α) => Rel.core r s ⊆ t) f.sets

theorem Filter.rcomap_rcomap {α : Type u} {β : Type v} {γ : Type w} (r : Rel α β) (s : Rel β γ) (l : Filter γ) : Filter.rcomap r (Filter.rcomap s l) = Filter.rcomap (Rel.comp r s) l

@[simp]

theorem Filter.rcomap_compose {α : Type u} {β : Type v} {γ : Type w} (r : Rel α β) (s : Rel β γ) : Filter.rcomap r ∘ Filter.rcomap s = Filter.rcomap (Rel.comp r s)

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 β) : Filter α

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

Equations

• Filter.rcomap' r f = { sets := Rel.image (fun (s : Set β) (t : Set α) => Rel.preimage r s ⊆ t) f.sets, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

@[simp]

theorem Filter.mem_rcomap' {α : Type u} {β : Type v} (r : Rel α β) (l : Filter β) (s : Set α) : s ∈ Filter.rcomap' r l ↔ ∃ t ∈ l, Rel.preimage r t ⊆ s

theorem Filter.rcomap'_sets {α : Type u} {β : Type v} (r : Rel α β) (f : Filter β) : (Filter.rcomap' r f).sets = Rel.image (fun (s : Set β) (t : Set α) => Rel.preimage r s ⊆ t) f.sets

@[simp]

theorem Filter.rcomap'_rcomap' {α : Type u} {β : Type v} {γ : Type w} (r : Rel α β) (s : Rel β γ) (l : Filter γ) : Filter.rcomap' r (Filter.rcomap' s l) = Filter.rcomap' (Rel.comp r s) l

@[simp]

theorem Filter.rcomap'_compose {α : Type u} {β : Type v} {γ : Type w} (r : Rel α β) (s : Rel β γ) : Filter.rcomap' r ∘ Filter.rcomap' s = Filter.rcomap' (Rel.comp r s)

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

• Filter.RTendsto' r l₁ l₂ = (l₁ ≤ Filter.rcomap' r l₂)

theorem Filter.rtendsto'_def {α : Type u} {β : Type v} (r : Rel α β) (l₁ : Filter α) (l₂ : Filter β) : Filter.RTendsto' r l₁ l₂ ↔ ∀ s ∈ l₂, Rel.preimage r s ∈ l₁

theorem Filter.tendsto_iff_rtendsto {α : Type u} {β : Type v} (l₁ : Filter α) (l₂ : Filter β) (f : α → β) : Filter.Tendsto f l₁ l₂ ↔ Filter.RTendsto (Function.graph f) l₁ l₂

theorem Filter.tendsto_iff_rtendsto' {α : Type u} {β : Type v} (l₁ : Filter α) (l₂ : Filter β) (f : α → β) : Filter.Tendsto f l₁ l₂ ↔ Filter.RTendsto' (Function.graph f) l₁ l₂

Partial functions

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

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

Equations

• Filter.pmap f l = Filter.rmap (PFun.graph' f) l

@[simp]

theorem Filter.mem_pmap {α : Type u} {β : Type v} (f : α →. β) (l : Filter α) (s : Set β) : s ∈ Filter.pmap f l ↔ PFun.core f 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

• Filter.PTendsto f l₁ l₂ = (Filter.pmap f l₁ ≤ l₂)

theorem Filter.ptendsto_def {α : Type u} {β : Type v} (f : α →. β) (l₁ : Filter α) (l₂ : Filter β) : Filter.PTendsto f l₁ l₂ ↔ ∀ s ∈ l₂, PFun.core f s ∈ l₁

theorem Filter.ptendsto_iff_rtendsto {α : Type u} {β : Type v} (l₁ : Filter α) (l₂ : Filter β) (f : α →. β) : Filter.PTendsto f l₁ l₂ ↔ Filter.RTendsto (PFun.graph' f) l₁ l₂

theorem Filter.pmap_res {α : Type u} {β : Type v} (l : Filter α) (s : Set α) (f : α → β) : Filter.pmap (PFun.res f s) l = Filter.map f (l ⊓ Filter.principal s)

theorem Filter.tendsto_iff_ptendsto {α : Type u} {β : Type v} (l₁ : Filter α) (l₂ : Filter β) (s : Set α) (f : α → β) : Filter.Tendsto f (l₁ ⊓ Filter.principal s) l₂ ↔ Filter.PTendsto (PFun.res f s) l₁ l₂

theorem Filter.tendsto_iff_ptendsto_univ {α : Type u} {β : Type v} (l₁ : Filter α) (l₂ : Filter β) (f : α → β) : Filter.Tendsto f l₁ l₂ ↔ Filter.PTendsto (PFun.res f Set.univ) l₁ l₂

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

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

Equations

• Filter.pcomap' f l = Filter.rcomap' (PFun.graph' f) 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-preimage of a is an l₁-neighborhood. One generalization of Filter.Tendsto to partial functions.

Equations

• Filter.PTendsto' f l₁ l₂ = (l₁ ≤ Filter.rcomap' (PFun.graph' f) l₂)

theorem Filter.ptendsto'_def {α : Type u} {β : Type v} (f : α →. β) (l₁ : Filter α) (l₂ : Filter β) : Filter.PTendsto' f l₁ l₂ ↔ ∀ s ∈ l₂, PFun.preimage f 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 : PFun.Dom f ∈ l₁) : Filter.PTendsto f l₁ l₂ → Filter.PTendsto' f l₁ l₂