# mathlib3documentation

data.analysis.filter

# Computational realization of filters (experimental) #

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

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)
• 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

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 cfilter
@[protected, instance]
def cfilter.inhabited {α : Type u_1} [inhabited α]  :
Equations
@[protected, instance]
def cfilter.has_coe_to_fun {α : Type u_1} {σ : Type u_3}  :
has_coe_to_fun (cfilter α σ) (λ (_x : σ), σ α)
Equations
@[simp]
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₂} a = f a
def cfilter.of_equiv {α : Type u_1} {σ : Type u_3} {τ : Type u_4} (E : σ τ) :
σ τ

Map a cfilter to an equivalent representation type.

Equations
@[simp]
theorem cfilter.of_equiv_val {α : Type u_1} {σ : Type u_3} {τ : Type u_4} (E : σ τ) (F : σ) (a : τ) :
F) a = F ((E.symm) a)
def cfilter.to_filter {α : 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
@[simp]
theorem cfilter.mem_to_filter_sets {α : Type u_1} {σ : Type u_3} (F : cfilter (set α) σ) {a : set α} :
a F.to_filter (b : σ), F b a
structure filter.realizer {α : Type u_1} (f : filter α) :
Type (max u_1 (u_5+1))

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

Instances for filter.realizer
@[protected]
def cfilter.to_realizer {α : Type u_1} {σ : Type u_3} (F : cfilter (set α) σ) :

A cfilter realizes the filter it generates.

Equations
theorem filter.realizer.mem_sets {α : Type u_1} {f : filter α} (F : f.realizer) {a : set α} :
a f (b : F.σ), (F.F) b a
def filter.realizer.of_eq {α : Type u_1} {f g : filter α} (e : f = g) (F : f.realizer) :

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

Equations
def filter.realizer.of_filter {α : Type u_1} (f : filter α) :

A filter realizes itself.

Equations
def filter.realizer.of_equiv {α : Type u_1} {τ : Type u_4} {f : filter α} (F : f.realizer) (E : F.σ τ) :

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

Equations
@[simp]
theorem filter.realizer.of_equiv_σ {α : Type u_1} {τ : Type u_4} {f : filter α} (F : f.realizer) (E : F.σ τ) :
(F.of_equiv E).σ = τ
@[simp]
theorem filter.realizer.of_equiv_F {α : Type u_1} {τ : Type u_4} {f : filter α} (F : f.realizer) (E : F.σ τ) (s : τ) :
((F.of_equiv E).F) s = (F.F) ((E.symm) s)
@[protected]
def filter.realizer.principal {α : Type u_1} (s : set α) :

unit is a realizer for the principal filter

Equations
@[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
@[protected, instance]
def filter.realizer.realizer.inhabited {α : Type u_1} (s : set α) :
Equations
@[protected]
def filter.realizer.top {α : Type u_1} :

unit is a realizer for the top filter

Equations
@[simp]
theorem filter.realizer.top_σ {α : Type u_1} :
@[simp]
theorem filter.realizer.top_F {α : Type u_1} (u : unit) :
@[protected]
def filter.realizer.bot {α : Type u_1} :

unit is a realizer for the bottom filter

Equations
@[simp]
theorem filter.realizer.bot_σ {α : Type u_1} :
@[simp]
theorem filter.realizer.bot_F {α : Type u_1} (u : unit) :
@[protected]
def filter.realizer.map {α : Type u_1} {β : Type u_2} (m : α β) {f : filter α} (F : f.realizer) :

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

Equations
@[simp]
theorem filter.realizer.map_σ {α : Type u_1} {β : Type u_2} (m : α β) {f : filter α} (F : f.realizer) :
F).σ = F.σ
@[simp]
theorem filter.realizer.map_F {α : Type u_1} {β : Type u_2} (m : α β) {f : filter α} (F : f.realizer) (s : F).σ) :
F).F) s = m '' (F.F) s
@[protected]
def filter.realizer.comap {α : Type u_1} {β : Type u_2} (m : α β) {f : filter β} (F : f.realizer) :

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

Equations
@[protected]
def filter.realizer.sup {α : Type u_1} {f g : filter α} (F : f.realizer) (G : g.realizer) :

Construct a realizer for the sup of two filters

Equations
• F.sup G = {σ := F.σ × G.σ, F := {f := λ (_x : F.σ × G.σ), filter.realizer.sup._match_1 F G _x, pt := (F.F.pt, G.F.pt), inf := λ (_x : F.σ × G.σ), filter.realizer.sup._match_3 F G _x, inf_le_left := _, inf_le_right := _}, eq := _}
• filter.realizer.sup._match_1 F G (s, t) = (F.F) s (G.F) t
• filter.realizer.sup._match_3 F G (a, a') = λ (_x : F.σ × G.σ), filter.realizer.sup._match_2 F G a a' _x
• filter.realizer.sup._match_2 F G a a' (b, b') = (F.F.inf a b, G.F.inf a' b')
@[protected]
def filter.realizer.inf {α : Type u_1} {f g : filter α} (F : f.realizer) (G : g.realizer) :

Construct a realizer for the inf of two filters

Equations
• F.inf G = {σ := F.σ × G.σ, F := {f := λ (_x : F.σ × G.σ), filter.realizer.inf._match_1 F G _x, pt := (F.F.pt, G.F.pt), inf := λ (_x : F.σ × G.σ), filter.realizer.inf._match_3 F G _x, inf_le_left := _, inf_le_right := _}, eq := _}
• filter.realizer.inf._match_1 F G (s, t) = (F.F) s (G.F) t
• filter.realizer.inf._match_3 F G (a, a') = λ (_x : F.σ × G.σ), filter.realizer.inf._match_2 F G a a' _x
• filter.realizer.inf._match_2 F G a a' (b, b') = (F.F.inf a b, G.F.inf a' b')
@[protected]
def filter.realizer.cofinite {α : Type u_1} [decidable_eq α] :

Construct a realizer for the cofinite filter

Equations
@[protected]
def filter.realizer.bind {α : Type u_1} {β : Type u_2} {f : filter α} {m : α } (F : f.realizer) (G : Π (i : α), (m i).realizer) :

Construct a realizer for filter bind

Equations
@[protected]
def filter.realizer.Sup {α : Type u_1} {β : Type u_2} {f : α } (F : Π (i : α), (f i).realizer) :
( (i : α), f i).realizer

Construct a realizer for indexed supremum

Equations
@[protected]
def filter.realizer.prod {α : Type u_1} {f g : filter α} (F : f.realizer) (G : g.realizer) :

Construct a realizer for the product of filters

Equations
theorem filter.realizer.le_iff {α : Type u_1} {f g : filter α} (F : f.realizer) (G : g.realizer) :
f g (b : G.σ), (a : F.σ), (F.F) a (G.F) b
theorem filter.realizer.tendsto_iff {α : Type u_1} {β : Type u_2} (f : α β) {l₁ : filter α} {l₂ : filter β} (L₁ : l₁.realizer) (L₂ : l₂.realizer) :
l₁ l₂ (b : L₂.σ), (a : L₁.σ), (x : α), x (L₁.F) a f x (L₂.F) b
theorem filter.realizer.ne_bot_iff {α : Type u_1} {f : filter α} (F : f.realizer) :
f (a : F.σ), ((F.F) a).nonempty