# Documentation

Mathlib.Data.Analysis.Filter

# Computational realization of filters (experimental) #

This file provides infrastructure to compute with filters.

## Main declarations #

• CFilter: Realization of a filter base. Note that this is in the generality of filters on lattices, while Filter is filters of sets (so corresponding to CFilter (Set α) σ).
• Filter.Realizer: Realization of a Filter. CFilter that generates the given filter.
structure CFilter (α : Type u_1) (σ : Type u_2) [] :
Type (max u_1 u_2)

A CFilter α σ is a realization of a filter (base) on α, represented by a type σ together with operations for the top element and the binary inf operation.

Instances For
instance CFilter.instCoeFunCFilterForAll {α : Type u_1} {σ : Type u_3} [] :
CoeFun (CFilter α σ) fun x => σα
theorem CFilter.coe_mk {α : Type u_1} {σ : Type u_3} [] (f : σα) (pt : σ) (inf : σσσ) (h₁ : ∀ (a b : σ), f (inf a b) f a) (h₂ : ∀ (a b : σ), f (inf a b) f b) (a : σ) :
CFilter.f { f := f, pt := pt, inf := inf, inf_le_left := h₁, inf_le_right := h₂ } a = f a
def CFilter.ofEquiv {α : Type u_1} {σ : Type u_3} {τ : Type u_4} [] (E : σ τ) :
CFilter α σCFilter α τ

Map a CFilter to an equivalent representation type.

Instances For
@[simp]
theorem CFilter.ofEquiv_val {α : Type u_1} {σ : Type u_3} {τ : Type u_4} [] (E : σ τ) (F : CFilter α σ) (a : τ) :
CFilter.f () a = CFilter.f F (E.symm a)
def CFilter.toFilter {α : Type u_1} {σ : Type u_3} (F : CFilter (Set α) σ) :

The filter represented by a CFilter is the collection of supersets of elements of the filter base.

Instances For
@[simp]
theorem CFilter.mem_toFilter_sets {α : Type u_1} {σ : Type u_3} (F : CFilter (Set α) σ) {a : Set α} :
b, a
structure Filter.Realizer {α : Type u_1} (f : ) :
Type (max u_1 (u_5 + 1))

A realizer for filter f is a cfilter which generates f.

Instances For
def CFilter.toRealizer {α : Type u_1} {σ : Type u_3} (F : CFilter (Set α) σ) :

A CFilter realizes the filter it generates.

Instances For
theorem Filter.Realizer.mem_sets {α : Type u_1} {f : } (F : ) {a : Set α} :
a f b, CFilter.f F.F b a
def Filter.Realizer.ofEq {α : Type u_1} {f : } {g : } (e : f = g) (F : ) :

Transfer a realizer along an equality of filter. This has better definitional equalities than the Eq.rec proof.

Instances For
def Filter.Realizer.ofFilter {α : Type u_1} (f : ) :

A filter realizes itself.

Instances For
def Filter.Realizer.ofEquiv {α : Type u_1} {τ : Type u_4} {f : } (F : ) (E : F τ) :

Transfer a filter realizer to another realizer on a different base type.

Instances For
@[simp]
theorem Filter.Realizer.ofEquiv_σ {α : Type u_1} {τ : Type u_4} {f : } (F : ) (E : F τ) :
().σ = τ
@[simp]
theorem Filter.Realizer.ofEquiv_F {α : Type u_1} {τ : Type u_4} {f : } (F : ) (E : F τ) (s : τ) :
CFilter.f ().F s = CFilter.f F.F (E.symm s)
def Filter.Realizer.principal {α : Type u_1} (s : Set α) :

Unit is a realizer for the principal filter

Instances For
@[simp]
theorem Filter.Realizer.principal_σ {α : Type u_1} (s : Set α) :
@[simp]
theorem Filter.Realizer.principal_F {α : Type u_1} (s : Set α) (u : Unit) :
= s
def Filter.Realizer.top {α : Type u_1} :

Unit is a realizer for the top filter

Instances For
@[simp]
theorem Filter.Realizer.top_σ {α : Type u_1} :
Filter.Realizer.top = Unit
@[simp]
theorem Filter.Realizer.top_F {α : Type u_1} (u : Unit) :
CFilter.f Filter.Realizer.top.F u = Set.univ
def Filter.Realizer.bot {α : Type u_1} :

Unit is a realizer for the bottom filter

Instances For
@[simp]
theorem Filter.Realizer.bot_σ {α : Type u_1} :
Filter.Realizer.bot = Unit
@[simp]
theorem Filter.Realizer.bot_F {α : Type u_1} (u : Unit) :
CFilter.f Filter.Realizer.bot.F u =
def Filter.Realizer.map {α : Type u_1} {β : Type u_2} (m : αβ) {f : } (F : ) :

Construct a realizer for map m f given a realizer for f

Instances For
@[simp]
theorem Filter.Realizer.map_σ {α : Type u_1} {β : Type u_2} (m : αβ) {f : } (F : ) :
().σ = F
@[simp]
theorem Filter.Realizer.map_F {α : Type u_1} {β : Type u_2} (m : αβ) {f : } (F : ) (s : ().σ) :
CFilter.f ().F s = m '' CFilter.f F.F s
def Filter.Realizer.comap {α : Type u_1} {β : Type u_2} (m : αβ) {f : } (F : ) :

Construct a realizer for comap m f given a realizer for f

Instances For
def Filter.Realizer.sup {α : Type u_1} {f : } {g : } (F : ) (G : ) :

Construct a realizer for the sup of two filters

Instances For
def Filter.Realizer.inf {α : Type u_1} {f : } {g : } (F : ) (G : ) :

Construct a realizer for the inf of two filters

Instances For
def Filter.Realizer.cofinite {α : Type u_1} [] :
Filter.Realizer Filter.cofinite

Construct a realizer for the cofinite filter

Instances For
def Filter.Realizer.bind {α : Type u_1} {β : Type u_2} {f : } {m : α} (F : ) (G : (i : α) → Filter.Realizer (m i)) :

Construct a realizer for filter bind

Instances For
def Filter.Realizer.iSup {α : Type u_1} {β : Type u_2} {f : α} (F : (i : α) → Filter.Realizer (f i)) :
Filter.Realizer (⨆ (i : α), f i)

Construct a realizer for indexed supremum

Instances For
def Filter.Realizer.prod {α : Type u_1} {f : } {g : } (F : ) (G : ) :

Construct a realizer for the product of filters

Instances For
theorem Filter.Realizer.le_iff {α : Type u_1} {f : } {g : } (F : ) (G : ) :
f g ∀ (b : G), a, CFilter.f F.F a CFilter.f G.F b
theorem Filter.Realizer.tendsto_iff {α : Type u_1} {β : Type u_2} (f : αβ) {l₁ : } {l₂ : } (L₁ : ) (L₂ : ) :
Filter.Tendsto f l₁ l₂ ∀ (b : L₂), a, ∀ (x : α), x CFilter.f L₁.F af x CFilter.f L₂.F b
theorem Filter.Realizer.ne_bot_iff {α : Type u_1} {f : } (F : ) :
f ∀ (a : F), Set.Nonempty (CFilter.f F.F a)