Equations
- filter.rmap r f = {sets := r.core ⁻¹' f.sets, univ_sets := _, sets_of_superset := _, inter_sets := _}
@[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 α) :
filter.rmap s (filter.rmap r l) = filter.rmap (r.comp s) l
@[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)
Equations
- filter.rtendsto r l₁ l₂ = (filter.rmap r l₁ ≤ l₂)
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 := _}
@[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
@[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)
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₂
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 := _}
@[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
@[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)
Equations
- filter.rtendsto' r l₁ l₂ = (l₁ ≤ filter.rcomap' r l₂)
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₂
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₂
Equations
- filter.pmap f l = filter.rmap f.graph' l
@[simp]
theorem
filter.mem_pmap
{α : Type u}
{β : Type v}
(f : α →. β)
(l : filter α)
(s : set β) :
s ∈ filter.pmap f l ↔ f.core s ∈ l
Equations
- filter.ptendsto f l₁ l₂ = (filter.pmap f l₁ ≤ 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 : α → β) :
filter.pmap (pfun.res f s) l = filter.map f (l ⊓ filter.principal s)
theorem
filter.tendsto_iff_ptendsto
{α : Type u}
{β : Type v}
(l₁ : filter α)
(l₂ : filter β)
(s : set α)
(f : α → β) :
filter.tendsto f (l₁ ⊓ filter.principal 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 : α → β) :
filter.tendsto f l₁ l₂ ↔ filter.ptendsto (pfun.res f set.univ) l₁ l₂
Equations
- filter.pcomap' f l = filter.rcomap' f.graph' l
Equations
- filter.ptendsto' f l₁ l₂ = (l₁ ≤ filter.rcomap' f.graph' 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₂