mathlib docs: order.filter.partial

source

def filter.rmap {α : Type u} {β : Type v} (r : rel α β) (f : filter α) :

filter β

Equations

filter.rmap r f = {sets := r.core ⁻¹' f.sets, univ_sets := _, sets_of_superset := _, inter_sets := _}

source

theorem filter.rmap_sets {α : Type u} {β : Type v} (r : rel α β) (f : filter α) :

(filter.rmap r f).sets = r.core ⁻¹' f.sets

source

@[simp]

theorem filter.mem_rmap {α : Type u} {β : Type v} (r : rel α β) (l : filter α) (s : set β) :

s ∈ filter.rmap r l ↔ r.core s ∈ l

source

@[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

source

@[simp]

theorem filter.rmap_compose {α : Type u} {β : Type v} {γ : Type w} (r : rel α β) (s : rel β γ) :

filter.rmap s ∘ filter.rmap r = filter.rmap (r.comp s)

source

def filter.rtendsto {α : Type u} {β : Type v} (r : rel α β) (l₁ : filter α) (l₂ : filter β) :

Prop

Equations

filter.rtendsto r l₁ l₂ = (filter.rmap r l₁ ≤ l₂)

source

theorem filter.rtendsto_def {α : Type u} {β : Type v} (r : rel α β) (l₁ : filter α) (l₂ : filter β) :

filter.rtendsto r l₁ l₂ ↔ ∀ (s : set β), s ∈ l₂ → r.core s ∈ l₁

source

def filter.rcomap {α : Type u} {β : Type v} (r : rel α β) (f : filter β) :

filter α

Equations

filter.rcomap r f = {sets := rel.image (λ (s : set β) (t : set α), r.core s ⊆ t) f.sets, univ_sets := _, sets_of_superset := _, inter_sets := _}

source

theorem filter.rcomap_sets {α : Type u} {β : Type v} (r : rel α β) (f : filter β) :

(filter.rcomap r f).sets = rel.image (λ (s : set β) (t : set α), r.core s ⊆ t) f.sets

source

@[simp]

theorem filter.rcomap_rcomap {α : Type u} {β : Type v} {γ : Type w} (r : rel α β) (s : rel β γ) (l : filter γ) :

filter.rcomap r (filter.rcomap s l) = filter.rcomap (r.comp s) l

source

@[simp]

theorem filter.rcomap_compose {α : Type u} {β : Type v} {γ : Type w} (r : rel α β) (s : rel β γ) :

filter.rcomap r ∘ filter.rcomap s = filter.rcomap (r.comp s)

source

theorem filter.rtendsto_iff_le_comap {α : Type u} {β : Type v} (r : rel α β) (l₁ : filter α) (l₂ : filter β) :

filter.rtendsto r l₁ l₂ ↔ l₁ ≤ filter.rcomap r l₂

source

def filter.rcomap' {α : Type u} {β : Type v} (r : rel α β) (f : filter β) :

filter α

Equations

filter.rcomap' r f = {sets := rel.image (λ (s : set β) (t : set α), r.preimage s ⊆ t) f.sets, univ_sets := _, sets_of_superset := _, inter_sets := _}

source

@[simp]

theorem filter.mem_rcomap' {α : Type u} {β : Type v} (r : rel α β) (l : filter β) (s : set α) :

s ∈ filter.rcomap' r l ↔ ∃ (t : set β) (H : t ∈ l), r.preimage t ⊆ s

source

theorem filter.rcomap'_sets {α : Type u} {β : Type v} (r : rel α β) (f : filter β) :

(filter.rcomap' r f).sets = rel.image (λ (s : set β) (t : set α), r.preimage s ⊆ t) f.sets

source

@[simp]

theorem filter.rcomap'_rcomap' {α : Type u} {β : Type v} {γ : Type w} (r : rel α β) (s : rel β γ) (l : filter γ) :

filter.rcomap' r (filter.rcomap' s l) = filter.rcomap' (r.comp s) l

source

@[simp]

theorem filter.rcomap'_compose {α : Type u} {β : Type v} {γ : Type w} (r : rel α β) (s : rel β γ) :

filter.rcomap' r ∘ filter.rcomap' s = filter.rcomap' (r.comp s)

source

def filter.rtendsto' {α : Type u} {β : Type v} (r : rel α β) (l₁ : filter α) (l₂ : filter β) :

Prop

Equations

filter.rtendsto' r l₁ l₂ = (l₁ ≤ filter.rcomap' r l₂)

source

theorem filter.rtendsto'_def {α : Type u} {β : Type v} (r : rel α β) (l₁ : filter α) (l₂ : filter β) :

filter.rtendsto' r l₁ l₂ ↔ ∀ (s : set β), s ∈ l₂ → r.preimage s ∈ l₁

source

theorem filter.tendsto_iff_rtendsto {α : Type u} {β : Type v} (l₁ : filter α) (l₂ : filter β) (f : α → β) :

filter.tendsto f l₁ l₂ ↔ filter.rtendsto (function.graph f) l₁ l₂

source

theorem filter.tendsto_iff_rtendsto' {α : Type u} {β : Type v} (l₁ : filter α) (l₂ : filter β) (f : α → β) :

filter.tendsto f l₁ l₂ ↔ filter.rtendsto' (function.graph f) l₁ l₂

source

def filter.pmap {α : Type u} {β : Type v} (f : α →. β) (l : filter α) :

filter β

Equations

filter.pmap f l = filter.rmap f.graph' l

source

@[simp]

theorem filter.mem_pmap {α : Type u} {β : Type v} (f : α →. β) (l : filter α) (s : set β) :

s ∈ filter.pmap f l ↔ f.core s ∈ l

source

def filter.ptendsto {α : Type u} {β : Type v} (f : α →. β) (l₁ : filter α) (l₂ : filter β) :

Prop

Equations

filter.ptendsto f l₁ l₂ = (filter.pmap f l₁ ≤ l₂)

source

theorem filter.ptendsto_def {α : Type u} {β : Type v} (f : α →. β) (l₁ : filter α) (l₂ : filter β) :

filter.ptendsto f l₁ l₂ ↔ ∀ (s : set β), s ∈ l₂ → f.core s ∈ l₁

source

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₂

source

theorem filter.pmap_res {α : Type u} {β : Type v} (l : filter α) (s : set α) (f : α → β) :

filter.pmap (pfun.res f s) l = filter.map f (l ⊓ 𝓟 s)

source

theorem filter.tendsto_iff_ptendsto {α : Type u} {β : Type v} (l₁ : filter α) (l₂ : filter β) (s : set α) (f : α → β) :

filter.tendsto f (l₁ ⊓ 𝓟 s) l₂ ↔ filter.ptendsto (pfun.res f s) l₁ l₂

source

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₂

source

def filter.pcomap' {α : Type u} {β : Type v} (f : α →. β) (l : filter β) :

filter α

Equations

filter.pcomap' f l = filter.rcomap' f.graph' l

source

def filter.ptendsto' {α : Type u} {β : Type v} (f : α →. β) (l₁ : filter α) (l₂ : filter β) :

Prop

Equations

filter.ptendsto' f l₁ l₂ = (l₁ ≤ filter.rcomap' f.graph' l₂)

source

theorem filter.ptendsto'_def {α : Type u} {β : Type v} (f : α →. β) (l₁ : filter α) (l₂ : filter β) :

filter.ptendsto' f l₁ l₂ ↔ ∀ (s : set β), s ∈ l₂ → f.preimage s ∈ l₁

source

theorem filter.ptendsto_of_ptendsto' {α : Type u} {β : Type v} {f : α →. β} {l₁ : filter α} {l₂ : filter β} (a : filter.ptendsto' f l₁ l₂) :

filter.ptendsto f l₁ l₂

source

theorem filter.ptendsto'_of_ptendsto {α : Type u} {β : Type v} {f : α →. β} {l₁ : filter α} {l₂ : filter β} (h : f.dom ∈ l₁) (a : filter.ptendsto f l₁ l₂) :

filter.ptendsto' f l₁ l₂