Convergence in terms of filters #
The general notion of limit of a map with respect to filters on the source and target types
is Filter.Tendsto. It is defined in terms of the order and the push-forward operation.
For instance, anticipating on Topology.Basic, the statement: "if a sequence u converges to
some x and u n belongs to a set M for n large enough then x is in the closure of
M" is formalized as: Tendsto u atTop (𝓝 x) → (∀ᶠ n in atTop, u n ∈ M) → x ∈ closure M,
which is a special case of mem_closure_of_tendsto from Topology/Basic.
theorem
Filter.tendsto_def
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{l₁ : Filter α}
{l₂ : Filter β}
:
Filter.Tendsto f l₁ l₂ ↔ ∀ s ∈ l₂, f ⁻¹' s ∈ l₁
theorem
Filter.tendsto_iff_eventually
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{l₁ : Filter α}
{l₂ : Filter β}
:
Filter.Tendsto f l₁ l₂ ↔ ∀ ⦃p : β → Prop⦄, (∀ᶠ (y : β) in l₂, p y) → ∀ᶠ (x : α) in l₁, p (f x)
theorem
Filter.tendsto_iff_forall_eventually_mem
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{l₁ : Filter α}
{l₂ : Filter β}
:
Filter.Tendsto f l₁ l₂ ↔ ∀ s ∈ l₂, ∀ᶠ (x : α) in l₁, f x ∈ s
theorem
Filter.Tendsto.eventually_mem
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{l₁ : Filter α}
{l₂ : Filter β}
{s : Set β}
(hf : Filter.Tendsto f l₁ l₂)
(h : s ∈ l₂)
:
∀ᶠ (x : α) in l₁, f x ∈ s
theorem
Filter.Tendsto.eventually
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{l₁ : Filter α}
{l₂ : Filter β}
{p : β → Prop}
(hf : Filter.Tendsto f l₁ l₂)
(h : ∀ᶠ (y : β) in l₂, p y)
:
∀ᶠ (x : α) in l₁, p (f x)
theorem
Filter.not_tendsto_iff_exists_frequently_nmem
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{l₁ : Filter α}
{l₂ : Filter β}
:
¬Filter.Tendsto f l₁ l₂ ↔ ∃ s ∈ l₂, ∃ᶠ (x : α) in l₁, f x ∉ s
theorem
Filter.Tendsto.frequently
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{l₁ : Filter α}
{l₂ : Filter β}
{p : β → Prop}
(hf : Filter.Tendsto f l₁ l₂)
(h : ∃ᶠ (x : α) in l₁, p (f x))
:
∃ᶠ (y : β) in l₂, p y
theorem
Filter.Tendsto.frequently_map
{α : Type u_1}
{β : Type u_2}
{l₁ : Filter α}
{l₂ : Filter β}
{p : α → Prop}
{q : β → Prop}
(f : α → β)
(c : Filter.Tendsto f l₁ l₂)
(w : ∀ (x : α), p x → q (f x))
(h : ∃ᶠ (x : α) in l₁, p x)
:
∃ᶠ (y : β) in l₂, q y
@[simp]
theorem
Filter.tendsto_bot
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{l : Filter β}
:
Filter.Tendsto f ⊥ l
theorem
Filter.Tendsto.of_neBot_imp
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{la : Filter α}
{lb : Filter β}
(h : la.NeBot → Filter.Tendsto f la lb)
:
Filter.Tendsto f la lb
@[simp]
theorem
Filter.tendsto_top
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{l : Filter α}
:
Filter.Tendsto f l ⊤
theorem
Filter.le_map_of_right_inverse
{α : Type u_1}
{β : Type u_2}
{mab : α → β}
{mba : β → α}
{f : Filter α}
{g : Filter β}
(h₁ : mab ∘ mba =ᶠ[g] id)
(h₂ : Filter.Tendsto mba g f)
:
g ≤ Filter.map mab f
theorem
Filter.tendsto_of_isEmpty
{α : Type u_1}
{β : Type u_2}
[IsEmpty α]
{f : α → β}
{la : Filter α}
{lb : Filter β}
:
Filter.Tendsto f la lb
theorem
Filter.tendsto_iff_comap
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{l₁ : Filter α}
{l₂ : Filter β}
:
Filter.Tendsto f l₁ l₂ ↔ l₁ ≤ Filter.comap f l₂
theorem
Filter.Tendsto.le_comap
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{l₁ : Filter α}
{l₂ : Filter β}
:
Filter.Tendsto f l₁ l₂ → l₁ ≤ Filter.comap f l₂
Alias of the forward direction of Filter.tendsto_iff_comap.
theorem
Filter.Tendsto.disjoint
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{la₁ la₂ : Filter α}
{lb₁ lb₂ : Filter β}
(h₁ : Filter.Tendsto f la₁ lb₁)
(hd : Disjoint lb₁ lb₂)
(h₂ : Filter.Tendsto f la₂ lb₂)
:
Disjoint la₁ la₂
theorem
Filter.tendsto_congr'
{α : Type u_1}
{β : Type u_2}
{f₁ f₂ : α → β}
{l₁ : Filter α}
{l₂ : Filter β}
(hl : f₁ =ᶠ[l₁] f₂)
:
Filter.Tendsto f₁ l₁ l₂ ↔ Filter.Tendsto f₂ l₁ l₂
theorem
Filter.Tendsto.congr'
{α : Type u_1}
{β : Type u_2}
{f₁ f₂ : α → β}
{l₁ : Filter α}
{l₂ : Filter β}
(hl : f₁ =ᶠ[l₁] f₂)
(h : Filter.Tendsto f₁ l₁ l₂)
:
Filter.Tendsto f₂ l₁ l₂
theorem
Filter.tendsto_congr
{α : Type u_1}
{β : Type u_2}
{f₁ f₂ : α → β}
{l₁ : Filter α}
{l₂ : Filter β}
(h : ∀ (x : α), f₁ x = f₂ x)
:
Filter.Tendsto f₁ l₁ l₂ ↔ Filter.Tendsto f₂ l₁ l₂
theorem
Filter.Tendsto.congr
{α : Type u_1}
{β : Type u_2}
{f₁ f₂ : α → β}
{l₁ : Filter α}
{l₂ : Filter β}
(h : ∀ (x : α), f₁ x = f₂ x)
:
Filter.Tendsto f₁ l₁ l₂ → Filter.Tendsto f₂ l₁ l₂
theorem
Filter.Tendsto.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{g : β → γ}
{x : Filter α}
{y : Filter β}
{z : Filter γ}
(hg : Filter.Tendsto g y z)
(hf : Filter.Tendsto f x y)
:
Filter.Tendsto (g ∘ f) x z
theorem
Filter.Tendsto.iterate
{α : Type u_1}
{f : α → α}
{l : Filter α}
(h : Filter.Tendsto f l l)
(n : ℕ)
:
Filter.Tendsto f^[n] l l
theorem
Filter.Tendsto.mono_left
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{x y : Filter α}
{z : Filter β}
(hx : Filter.Tendsto f x z)
(h : y ≤ x)
:
Filter.Tendsto f y z
theorem
Filter.Tendsto.mono_right
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{x : Filter α}
{y z : Filter β}
(hy : Filter.Tendsto f x y)
(hz : y ≤ z)
:
Filter.Tendsto f x z
theorem
Filter.Tendsto.neBot
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{x : Filter α}
{y : Filter β}
(h : Filter.Tendsto f x y)
[hx : x.NeBot]
:
y.NeBot
theorem
Filter.tendsto_map
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{x : Filter α}
:
Filter.Tendsto f x (Filter.map f x)
@[simp]
theorem
Filter.tendsto_map'_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : β → γ}
{g : α → β}
{x : Filter α}
{y : Filter γ}
:
Filter.Tendsto f (Filter.map g x) y ↔ Filter.Tendsto (f ∘ g) x y
theorem
Filter.tendsto_map'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : β → γ}
{g : α → β}
{x : Filter α}
{y : Filter γ}
:
Filter.Tendsto (f ∘ g) x y → Filter.Tendsto f (Filter.map g x) y
Alias of the reverse direction of Filter.tendsto_map'_iff.
theorem
Filter.tendsto_comap
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{x : Filter β}
:
Filter.Tendsto f (Filter.comap f x) x
@[simp]
theorem
Filter.tendsto_comap_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{g : β → γ}
{a : Filter α}
{c : Filter γ}
:
Filter.Tendsto f a (Filter.comap g c) ↔ Filter.Tendsto (g ∘ f) a c
theorem
Filter.tendsto_comap'_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : α → β}
{f : Filter α}
{g : Filter β}
{i : γ → α}
(h : Set.range i ∈ f)
:
Filter.Tendsto (m ∘ i) (Filter.comap i f) g ↔ Filter.Tendsto m f g
theorem
Filter.Tendsto.of_tendsto_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{g : β → γ}
{a : Filter α}
{b : Filter β}
{c : Filter γ}
(hfg : Filter.Tendsto (g ∘ f) a c)
(hg : Filter.comap g c ≤ b)
:
Filter.Tendsto f a b
theorem
Filter.comap_eq_of_inverse
{α : Type u_1}
{β : Type u_2}
{f : Filter α}
{g : Filter β}
{φ : α → β}
(ψ : β → α)
(eq : ψ ∘ φ = id)
(hφ : Filter.Tendsto φ f g)
(hψ : Filter.Tendsto ψ g f)
:
Filter.comap φ g = f
theorem
Filter.map_eq_of_inverse
{α : Type u_1}
{β : Type u_2}
{f : Filter α}
{g : Filter β}
{φ : α → β}
(ψ : β → α)
(eq : φ ∘ ψ = id)
(hφ : Filter.Tendsto φ f g)
(hψ : Filter.Tendsto ψ g f)
:
Filter.map φ f = g
theorem
Filter.tendsto_inf
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{x : Filter α}
{y₁ y₂ : Filter β}
:
Filter.Tendsto f x (y₁ ⊓ y₂) ↔ Filter.Tendsto f x y₁ ∧ Filter.Tendsto f x y₂
theorem
Filter.tendsto_inf_left
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{x₁ x₂ : Filter α}
{y : Filter β}
(h : Filter.Tendsto f x₁ y)
:
Filter.Tendsto f (x₁ ⊓ x₂) y
theorem
Filter.tendsto_inf_right
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{x₁ x₂ : Filter α}
{y : Filter β}
(h : Filter.Tendsto f x₂ y)
:
Filter.Tendsto f (x₁ ⊓ x₂) y
theorem
Filter.Tendsto.inf
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{x₁ x₂ : Filter α}
{y₁ y₂ : Filter β}
(h₁ : Filter.Tendsto f x₁ y₁)
(h₂ : Filter.Tendsto f x₂ y₂)
:
Filter.Tendsto f (x₁ ⊓ x₂) (y₁ ⊓ y₂)
@[simp]
theorem
Filter.tendsto_iInf
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{f : α → β}
{x : Filter α}
{y : ι → Filter β}
:
Filter.Tendsto f x (⨅ (i : ι), y i) ↔ ∀ (i : ι), Filter.Tendsto f x (y i)
theorem
Filter.tendsto_iInf'
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{f : α → β}
{x : ι → Filter α}
{y : Filter β}
(i : ι)
(hi : Filter.Tendsto f (x i) y)
:
Filter.Tendsto f (⨅ (i : ι), x i) y
theorem
Filter.tendsto_iInf_iInf
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{f : α → β}
{x : ι → Filter α}
{y : ι → Filter β}
(h : ∀ (i : ι), Filter.Tendsto f (x i) (y i))
:
Filter.Tendsto f (iInf x) (iInf y)
@[simp]
theorem
Filter.tendsto_sup
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{x₁ x₂ : Filter α}
{y : Filter β}
:
Filter.Tendsto f (x₁ ⊔ x₂) y ↔ Filter.Tendsto f x₁ y ∧ Filter.Tendsto f x₂ y
theorem
Filter.Tendsto.sup
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{x₁ x₂ : Filter α}
{y : Filter β}
:
Filter.Tendsto f x₁ y → Filter.Tendsto f x₂ y → Filter.Tendsto f (x₁ ⊔ x₂) y
theorem
Filter.Tendsto.sup_sup
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{x₁ x₂ : Filter α}
{y₁ y₂ : Filter β}
(h₁ : Filter.Tendsto f x₁ y₁)
(h₂ : Filter.Tendsto f x₂ y₂)
:
Filter.Tendsto f (x₁ ⊔ x₂) (y₁ ⊔ y₂)
@[simp]
theorem
Filter.tendsto_iSup
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{f : α → β}
{x : ι → Filter α}
{y : Filter β}
:
Filter.Tendsto f (⨆ (i : ι), x i) y ↔ ∀ (i : ι), Filter.Tendsto f (x i) y
theorem
Filter.tendsto_iSup_iSup
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{f : α → β}
{x : ι → Filter α}
{y : ι → Filter β}
(h : ∀ (i : ι), Filter.Tendsto f (x i) (y i))
:
Filter.Tendsto f (iSup x) (iSup y)
@[simp]
theorem
Filter.tendsto_principal
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{l : Filter α}
{s : Set β}
:
Filter.Tendsto f l (Filter.principal s) ↔ ∀ᶠ (a : α) in l, f a ∈ s
theorem
Filter.tendsto_principal_principal
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{s : Set α}
{t : Set β}
:
Filter.Tendsto f (Filter.principal s) (Filter.principal t) ↔ ∀ a ∈ s, f a ∈ t
@[simp]
theorem
Filter.tendsto_pure
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{a : Filter α}
{b : β}
:
Filter.Tendsto f a (pure b) ↔ ∀ᶠ (x : α) in a, f x = b
theorem
Filter.tendsto_pure_pure
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(a : α)
:
Filter.Tendsto f (pure a) (pure (f a))
theorem
Filter.tendsto_const_pure
{α : Type u_1}
{β : Type u_2}
{a : Filter α}
{b : β}
:
Filter.Tendsto (fun (x : α) => b) a (pure b)
theorem
Filter.tendsto_pure_left
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{a : α}
{l : Filter β}
:
Filter.Tendsto f (pure a) l ↔ ∀ s ∈ l, f a ∈ s
@[simp]
theorem
Filter.map_inf_principal_preimage
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{s : Set β}
{l : Filter α}
:
Filter.map f (l ⊓ Filter.principal (f ⁻¹' s)) = Filter.map f l ⊓ Filter.principal s
theorem
Filter.Tendsto.not_tendsto
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{a : Filter α}
{b₁ b₂ : Filter β}
(hf : Filter.Tendsto f a b₁)
[a.NeBot]
(hb : Disjoint b₁ b₂)
:
¬Filter.Tendsto f a b₂
If two filters are disjoint, then a function cannot tend to both of them along a non-trivial filter.
theorem
Filter.Tendsto.if
{α : Type u_1}
{β : Type u_2}
{l₁ : Filter α}
{l₂ : Filter β}
{f g : α → β}
{p : α → Prop}
[(x : α) → Decidable (p x)]
(h₀ : Filter.Tendsto f (l₁ ⊓ Filter.principal {x : α | p x}) l₂)
(h₁ : Filter.Tendsto g (l₁ ⊓ Filter.principal {x : α | ¬p x}) l₂)
:
Filter.Tendsto (fun (x : α) => if p x then f x else g x) l₁ l₂
theorem
Filter.Tendsto.if'
{α : Type u_5}
{β : Type u_6}
{l₁ : Filter α}
{l₂ : Filter β}
{f g : α → β}
{p : α → Prop}
[DecidablePred p]
(hf : Filter.Tendsto f l₁ l₂)
(hg : Filter.Tendsto g l₁ l₂)
:
Filter.Tendsto (fun (a : α) => if p a then f a else g a) l₁ l₂
theorem
Filter.Tendsto.piecewise
{α : Type u_1}
{β : Type u_2}
{l₁ : Filter α}
{l₂ : Filter β}
{f g : α → β}
{s : Set α}
[(x : α) → Decidable (x ∈ s)]
(h₀ : Filter.Tendsto f (l₁ ⊓ Filter.principal s) l₂)
(h₁ : Filter.Tendsto g (l₁ ⊓ Filter.principal sᶜ) l₂)
:
Filter.Tendsto (s.piecewise f g) l₁ l₂
theorem
Set.MapsTo.tendsto
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{f : α → β}
(h : Set.MapsTo f s t)
:
Filter.Tendsto f (Filter.principal s) (Filter.principal t)
theorem
Filter.map_mapsTo_Iic_iff_tendsto
{α : Type u_1}
{β : Type u_2}
{F : Filter α}
{G : Filter β}
{m : α → β}
:
Set.MapsTo (Filter.map m) (Set.Iic F) (Set.Iic G) ↔ Filter.Tendsto m F G
theorem
Filter.Tendsto.map_mapsTo_Iic
{α : Type u_1}
{β : Type u_2}
{F : Filter α}
{G : Filter β}
{m : α → β}
:
Filter.Tendsto m F G → Set.MapsTo (Filter.map m) (Set.Iic F) (Set.Iic G)
Alias of the reverse direction of Filter.map_mapsTo_Iic_iff_tendsto.
theorem
Filter.map_mapsTo_Iic_iff_mapsTo
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{m : α → β}
:
Set.MapsTo (Filter.map m) (Set.Iic (Filter.principal s)) (Set.Iic (Filter.principal t)) ↔ Set.MapsTo m s t
theorem
Set.MapsTo.filter_map_Iic
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
{m : α → β}
:
Set.MapsTo m s t → Set.MapsTo (Filter.map m) (Set.Iic (Filter.principal s)) (Set.Iic (Filter.principal t))
Alias of the reverse direction of Filter.map_mapsTo_Iic_iff_mapsTo.