mathlib documentation

data.analysis.filter

structure cfilter (α : Type u_1) (σ : Type u_2) [partial_order α] :
Type (max u_1 u_2)
  • f : σ → α
  • pt : σ
  • inf : σ → σ → σ
  • inf_le_left : ∀ (a b : σ), c.f (c.inf a b) c.f a
  • inf_le_right : ∀ (a b : σ), c.f (c.inf a b) c.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.

@[instance]
def cfilter.has_coe_to_fun {α : Type u_1} {σ : Type u_3} [partial_order α] :

Equations
@[simp]
theorem cfilter.coe_mk {α : Type u_1} {σ : Type u_3} [partial_order α] (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} [partial_order α] :
σ τcfilter α σcfilter α τ

Map a cfilter to an equivalent representation type.

Equations
@[simp]
theorem cfilter.of_equiv_val {α : Type u_1} {σ : Type u_3} {τ : Type u_4} [partial_order α] (E : σ τ) (F : cfilter α σ) (a : τ) :
(cfilter.of_equiv E F) a = F ((E.symm) a)

def cfilter.to_filter {α : Type u_1} {σ : Type u_3} :
cfilter (set α) σfilter α

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} :
filter αType (max u_1 (u_5+1))

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

def cfilter.to_realizer {α : Type u_1} {σ : Type u_3} (F : cfilter (set α) σ) :

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 α} :
f = gf.realizer → g.realizer

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) :
F.σ τ → f.realizer

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)

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

@[simp]
theorem filter.realizer.top_σ {α : Type u_1} :

@[simp]
theorem filter.realizer.top_F {α : Type u_1} (u : unit) :

@[simp]
theorem filter.realizer.bot_σ {α : Type u_1} :

@[simp]
theorem filter.realizer.bot_F {α : Type u_1} (u : unit) :

def filter.realizer.map {α : Type u_1} {β : Type u_2} (m : α → β) {f : filter α} :

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

@[simp]
theorem filter.realizer.map_F {α : Type u_1} {β : Type u_2} (m : α → β) {f : filter α} (F : f.realizer) (s : (filter.realizer.map m F).σ) :
((filter.realizer.map m F).F) s = m '' (F.F) s

def filter.realizer.comap {α : Type u_1} {β : Type u_2} (m : α → β) {f : filter β} :

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

Equations
def filter.realizer.sup {α : Type u_1} {f g : filter α} :
f.realizerg.realizer(f 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')
def filter.realizer.inf {α : Type u_1} {f g : filter α} :
f.realizerg.realizer(f 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')

Construct a realizer for the cofinite filter

Equations
def filter.realizer.bind {α : Type u_1} {β : Type u_2} {f : filter α} {m : α → filter β} :
f.realizer(Π (i : α), (m i).realizer)(f.bind m).realizer

Construct a realizer for filter bind

Equations
  • F.bind G = {σ := Σ (s : F.σ), Π (i : α), i (F.F) s(G i).σ, F := {f := λ (_x : Σ (s : F.σ), Π (i : α), i (F.F) s(G i).σ), filter.realizer.bind._match_1 F G _x, pt := F.F.pt, λ (i : α) (H : i (F.F) F.F.pt), (G i).F.pt, inf := λ (_x : Σ (s : F.σ), Π (i : α), i (F.F) s(G i).σ), filter.realizer.bind._match_3 F G _x, inf_le_left := _, inf_le_right := _}, eq := _}
  • filter.realizer.bind._match_1 F G s, f_1⟩ = ⋃ (i : α) (H : i (F.F) s), ((G i).F) (f_1 i H)
  • filter.realizer.bind._match_3 F G a, f_1⟩ = λ (_x : Σ (s : F.σ), Π (i : α), i (F.F) s(G i).σ), filter.realizer.bind._match_2 F G a f_1 _x
  • filter.realizer.bind._match_2 F G a f_1 b, f'⟩ = F.F.inf a b, λ (i : α) (h : i (F.F) (F.F.inf a b)), (G i).F.inf (f_1 i _) (f' i _)
def filter.realizer.Sup {α : Type u_1} {β : Type u_2} {f : α → filter β} :
(Π (i : α), (f i).realizer)(⨆ (i : α), f i).realizer

Construct a realizer for indexed supremum

Equations
def filter.realizer.prod {α : Type u_1} {f g : filter α} :
f.realizerg.realizer(f ×ᶠ 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) :
filter.tendsto f l₁ l₂ ∀ (b : L₂.σ), ∃ (a : L₁.σ), ∀ (x : α), x (L₁.F) af 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