# 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.

• f : σα
• pt : σ
• inf : σσσ
• inf_le_left : ∀ (a b : σ), self.f (self.inf a b) self.f a
• inf_le_right : ∀ (a b : σ), self.f (self.inf a b) self.f b
Instances For
theorem CFilter.inf_le_left {α : Type u_1} {σ : Type u_2} [] (self : CFilter α σ) (a : σ) (b : σ) :
self.f (self.inf a b) self.f a
theorem CFilter.inf_le_right {α : Type u_1} {σ : Type u_2} [] (self : CFilter α σ) (a : σ) (b : σ) :
self.f (self.inf a b) self.f b
instance instInhabitedCFilter {α : Type u_1} [] [] :
Equations
• instInhabitedCFilter = { default := { f := id, pt := default, inf := fun (x1 x2 : α) => x1 x2, inf_le_left := , inf_le_right := } }
instance CFilter.instCoeFunForall {α : Type u_1} {σ : Type u_3} [] :
CoeFun (CFilter α σ) fun (x : CFilter α σ) => σα
Equations
• CFilter.instCoeFunForall = { coe := CFilter.f }
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 : σ) :
{ f := f, pt := pt, inf := inf, inf_le_left := h₁, inf_le_right := h₂ }.f 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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CFilter.ofEquiv_val {α : Type u_1} {σ : Type u_3} {τ : Type u_4} [] (E : σ τ) (F : CFilter α σ) (a : τ) :
(CFilter.ofEquiv E F).f a = 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.

Equations
• F.toFilter = { sets := {a : Set α | ∃ (b : σ), F.f b a}, univ_sets := , sets_of_superset := , inter_sets := }
Instances For
@[simp]
theorem CFilter.mem_toFilter_sets {α : Type u_1} {σ : Type u_3} (F : CFilter (Set α) σ) {a : Set α} :
a F.toFilter ∃ (b : σ), F.f 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
theorem Filter.Realizer.eq {α : Type u_1} {f : } (self : f.Realizer) :
self.F.toFilter = f
def CFilter.toRealizer {α : Type u_1} {σ : Type u_3} (F : CFilter (Set α) σ) :
F.toFilter.Realizer

A CFilter realizes the filter it generates.

Equations
• F.toRealizer = { σ := σ, F := F, eq := }
Instances For
theorem Filter.Realizer.mem_sets {α : Type u_1} {f : } (F : f.Realizer) {a : Set α} :
a f ∃ (b : F), F.F.f b a
def Filter.Realizer.ofEq {α : Type u_1} {f : } {g : } (e : f = g) (F : f.Realizer) :
g.Realizer

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

Equations
• = { σ := F, F := F.F, eq := }
Instances For
def Filter.Realizer.ofFilter {α : Type u_1} (f : ) :
f.Realizer

A filter realizes itself.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Filter.Realizer.ofEquiv {α : Type u_1} {τ : Type u_4} {f : } (F : f.Realizer) (E : F τ) :
f.Realizer

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

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

Unit is a realizer for the principal filter

Equations
• = { σ := Unit, F := { f := fun (x : Unit) => s, pt := (), inf := fun (x x : Unit) => (), inf_le_left := , inf_le_right := }, eq := }
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) :
.f u = s
instance Filter.Realizer.instInhabitedPrincipal {α : Type u_1} (s : Set α) :
Inhabited .Realizer
Equations
• = { default := }
def Filter.Realizer.top {α : Type u_1} :
.Realizer

Unit is a realizer for the top filter

Equations
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) :
Filter.Realizer.top.F.f u = Set.univ
def Filter.Realizer.bot {α : Type u_1} :
.Realizer

Unit is a realizer for the bottom filter

Equations
• Filter.Realizer.bot =
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) :
Filter.Realizer.bot.F.f u =
def Filter.Realizer.map {α : Type u_1} {β : Type u_2} (m : αβ) {f : } (F : f.Realizer) :
(Filter.map m f).Realizer

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

Equations
• = { σ := F, F := { f := fun (s : F) => m '' F.F.f s, pt := F.F.pt, inf := F.F.inf, inf_le_left := , inf_le_right := }, eq := }
Instances For
@[simp]
theorem Filter.Realizer.map_σ {α : Type u_1} {β : Type u_2} (m : αβ) {f : } (F : f.Realizer) :
= F
@[simp]
theorem Filter.Realizer.map_F {α : Type u_1} {β : Type u_2} (m : αβ) {f : } (F : f.Realizer) (s : ) :
.F.f s = m '' F.F.f s
def Filter.Realizer.comap {α : Type u_1} {β : Type u_2} (m : αβ) {f : } (F : f.Realizer) :
(Filter.comap m f).Realizer

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

Equations
• = { σ := F, F := { f := fun (s : F) => m ⁻¹' F.F.f s, pt := F.F.pt, inf := F.F.inf, inf_le_left := , inf_le_right := }, eq := }
Instances For
def Filter.Realizer.sup {α : Type u_1} {f : } {g : } (F : f.Realizer) (G : g.Realizer) :
(f g).Realizer

Construct a realizer for the sup of two filters

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Filter.Realizer.inf {α : Type u_1} {f : } {g : } (F : f.Realizer) (G : g.Realizer) :
(f g).Realizer

Construct a realizer for the inf of two filters

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Filter.Realizer.cofinite {α : Type u_1} [] :
Filter.cofinite.Realizer

Construct a realizer for the cofinite filter

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Filter.Realizer.bind {α : Type u_1} {β : Type u_2} {f : } {m : α} (F : f.Realizer) (G : (i : α) → (m i).Realizer) :
(f.bind m).Realizer

Construct a realizer for filter bind

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Filter.Realizer.iSup {α : Type u_1} {β : Type u_2} {f : α} (F : (i : α) → (f i).Realizer) :
(⨆ (i : α), f i).Realizer

Construct a realizer for indexed supremum

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Filter.Realizer.prod {α : Type u_1} {f : } {g : } (F : f.Realizer) (G : g.Realizer) :
(f.prod g).Realizer

Construct a realizer for the product of filters

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