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
  • Filter.rmap r l = { sets := {s : Set β | r.core s l}, univ_sets := , sets_of_superset := , inter_sets := }
Instances For
    theorem Filter.rmap_sets {α : Type u} {β : Type v} (r : Rel α β) (l : Filter α) :
    (Filter.rmap r l).sets = r.core ⁻¹' l.sets
    @[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 α) :
    Filter.rmap s (Filter.rmap r l) = Filter.rmap (r.comp s) l
    @[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 β) :

    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
    Instances For
      theorem Filter.rtendsto_def {α : Type u} {β : Type v} (r : Rel α β) (l₁ : Filter α) (l₂ : Filter β) :
      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
      • Filter.rcomap r f = { sets := Rel.image (fun (s : Set β) (t : Set α) => r.core s t) f.sets, univ_sets := , sets_of_superset := , inter_sets := }
      Instances For
        theorem Filter.rcomap_sets {α : Type u} {β : Type v} (r : Rel α β) (f : Filter β) :
        (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 γ) :
        @[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
        • Filter.rcomap' r f = { sets := Rel.image (fun (s : Set β) (t : Set α) => r.preimage s t) f.sets, univ_sets := , sets_of_superset := , inter_sets := }
        Instances For
          @[simp]
          theorem Filter.mem_rcomap' {α : Type u} {β : Type v} (r : Rel α β) (l : Filter β) (s : Set α) :
          s Filter.rcomap' r l tl, r.preimage 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 α) => 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 β) :

          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
          Instances For
            theorem Filter.rtendsto'_def {α : Type u} {β : Type v} (r : Rel α β) (l₁ : Filter α) (l₂ : Filter β) :
            Filter.RTendsto' r l₁ l₂ sl₂, 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
            Instances For
              @[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 β) :

              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
              Instances For
                theorem Filter.ptendsto_def {α : Type u} {β : Type v} (f : α →. β) (l₁ : Filter α) (l₂ : Filter β) :
                Filter.PTendsto f l₁ l₂ sl₂, 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 : αβ) :
                Filter.Tendsto f l₁ l₂ Filter.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
                Instances For
                  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
                  Instances For
                    theorem Filter.ptendsto'_def {α : Type u} {β : Type v} (f : α →. β) (l₁ : Filter α) (l₂ : Filter β) :
                    Filter.PTendsto' f l₁ l₂ sl₂, 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₂