mathlib documentation

order.filter.partial

def filter.rmap {α : Type u} {β : Type v} :
rel α βfilter αfilter β

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

@[simp]
theorem filter.mem_rmap {α : Type u} {β : Type v} (r : rel α β) (l : filter α) (s : set β) :
s filter.rmap r l r.core s l

@[simp]
theorem filter.rmap_rmap {α : Type u} {β : Type v} {γ : Type w} (r : rel α β) (s : rel β γ) (l : filter α) :

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

def filter.rtendsto {α : Type u} {β : Type v} :
rel α βfilter αfilter β → Prop

Equations
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₁

def filter.rcomap {α : Type u} {β : Type v} :
rel α βfilter βfilter α

Equations
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

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

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

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₂

def filter.rcomap' {α : Type u} {β : Type v} :
rel α βfilter βfilter α

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

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

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

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

def filter.rtendsto' {α : Type u} {β : Type v} :
rel α βfilter αfilter β → Prop

Equations
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₁

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

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

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

Equations
@[simp]
theorem filter.mem_pmap {α : Type u} {β : Type v} (f : α →. β) (l : filter α) (s : set β) :
s filter.pmap f l f.core s l

def filter.ptendsto {α : Type u} {β : Type v} :
→. β)filter αfilter β → Prop

Equations
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₁

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₂

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

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₂

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

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

Equations
def filter.ptendsto' {α : Type u} {β : Type v} :
→. β)filter αfilter β → Prop

Equations
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₁

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

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