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 β} : 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 β} : 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 β} : 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 : 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 : Tendsto f l₁ l₂) (h : ∀ᶠ (y : β) in l₂, p y) : ∀ᶠ (x : α) in l₁, p (f x)

theorem Filter.not_tendsto_iff_exists_frequently_notMem {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : 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 : 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 : 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 β} : Tendsto f ⊥ l

@[simp]

theorem Filter.tendsto_bot_right_iff {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter α} : Tendsto f l ⊥ ↔ l = ⊥

theorem Filter.Tendsto.of_neBot_imp {α : Type u_1} {β : Type u_2} {f : α → β} {la : Filter α} {lb : Filter β} (h : la.NeBot → Tendsto f la lb) : Tendsto f la lb

@[simp]

theorem Filter.tendsto_top {α : Type u_1} {β : Type u_2} {f : α → β} {l : 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₂ : Tendsto mba g f) : g ≤ map mab f

theorem Filter.tendsto_of_isEmpty {α : Type u_1} {β : Type u_2} [IsEmpty α] {f : α → β} {la : Filter α} {lb : Filter β} : Tendsto f la lb

theorem Filter.eventuallyEq_of_left_inv_of_right_inv {α : Type u_1} {β : Type u_2} {f : α → β} {g₁ g₂ : β → α} {fa : Filter α} {fb : Filter β} (hleft : ∀ᶠ (x : α) in fa, g₁ (f x) = x) (hright : ∀ᶠ (y : β) in fb, f (g₂ y) = y) (htendsto : Tendsto g₂ fb fa) : g₁ =ᶠ[fb] g₂

theorem Filter.tendsto_iff_comap {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} : Tendsto f l₁ l₂ ↔ l₁ ≤ comap f l₂

theorem Filter.Tendsto.le_comap {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} : Tendsto f l₁ l₂ → l₁ ≤ 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₁ : Tendsto f la₁ lb₁) (hd : Disjoint lb₁ lb₂) (h₂ : 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₂) : Tendsto f₁ l₁ l₂ ↔ 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 : Tendsto f₁ l₁ l₂) : 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) : Tendsto f₁ l₁ l₂ ↔ 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) : Tendsto f₁ l₁ l₂ → Tendsto f₂ l₁ l₂

theorem Filter.tendsto_id' {α : Type u_1} {x y : Filter α} : Tendsto id x y ↔ x ≤ y

theorem Filter.tendsto_id {α : Type u_1} {x : Filter α} : Tendsto id x x

theorem Filter.Tendsto.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} {x : Filter α} {y : Filter β} {z : Filter γ} (hg : Tendsto g y z) (hf : Tendsto f x y) : Tendsto (g ∘ f) x z

theorem Filter.Tendsto.iterate {α : Type u_1} {f : α → α} {l : Filter α} (h : Tendsto f l l) (n : ℕ) : Tendsto f^[n] l l

theorem Filter.Tendsto.mono_left {α : Type u_1} {β : Type u_2} {f : α → β} {x y : Filter α} {z : Filter β} (hx : Tendsto f x z) (h : y ≤ x) : Tendsto f y z

theorem Filter.Tendsto.mono_right {α : Type u_1} {β : Type u_2} {f : α → β} {x : Filter α} {y z : Filter β} (hy : Tendsto f x y) (hz : y ≤ z) : Tendsto f x z

theorem Filter.Tendsto.neBot {α : Type u_1} {β : Type u_2} {f : α → β} {x : Filter α} {y : Filter β} (h : Tendsto f x y) [hx : x.NeBot] : y.NeBot

theorem Filter.tendsto_map {α : Type u_1} {β : Type u_2} {f : α → β} {x : Filter α} : Tendsto f x (map f x)

@[simp]

theorem Filter.tendsto_map'_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} {g : α → β} {x : Filter α} {y : Filter γ} : Tendsto f (map g x) y ↔ Tendsto (f ∘ g) x y

theorem Filter.tendsto_map' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} {g : α → β} {x : Filter α} {y : Filter γ} : Tendsto (f ∘ g) x y → Tendsto f (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 β} : Tendsto f (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 γ} : Tendsto f a (comap g c) ↔ 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) : Tendsto (m ∘ i) (comap i f) g ↔ 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 : Tendsto (g ∘ f) a c) (hg : comap g c ≤ b) : Tendsto f a b

theorem Filter.comap_eq_of_inverse {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {φ : α → β} (ψ : β → α) (eq : ψ ∘ φ = id) (hφ : Tendsto φ f g) (hψ : Tendsto ψ g f) : comap φ g = f

theorem Filter.map_eq_of_inverse {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {φ : α → β} (ψ : β → α) (eq : φ ∘ ψ = id) (hφ : Tendsto φ f g) (hψ : Tendsto ψ g f) : map φ f = g

theorem Filter.tendsto_inf {α : Type u_1} {β : Type u_2} {f : α → β} {x : Filter α} {y₁ y₂ : Filter β} : Tendsto f x (y₁ ⊓ y₂) ↔ Tendsto f x y₁ ∧ Tendsto f x y₂

theorem Filter.tendsto_inf_left {α : Type u_1} {β : Type u_2} {f : α → β} {x₁ x₂ : Filter α} {y : Filter β} (h : Tendsto f x₁ y) : Tendsto f (x₁ ⊓ x₂) y

theorem Filter.tendsto_inf_right {α : Type u_1} {β : Type u_2} {f : α → β} {x₁ x₂ : Filter α} {y : Filter β} (h : Tendsto f x₂ y) : Tendsto f (x₁ ⊓ x₂) y

theorem Filter.Tendsto.inf {α : Type u_1} {β : Type u_2} {f : α → β} {x₁ x₂ : Filter α} {y₁ y₂ : Filter β} (h₁ : Tendsto f x₁ y₁) (h₂ : Tendsto f x₂ y₂) : 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 β} : Tendsto f x (⨅ (i : ι), y i) ↔ ∀ (i : ι), 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 : Tendsto f (x i) y) : 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 : ι), Tendsto f (x i) (y i)) : Tendsto f (iInf x) (iInf y)

@[simp]

theorem Filter.tendsto_sup {α : Type u_1} {β : Type u_2} {f : α → β} {x₁ x₂ : Filter α} {y : Filter β} : Tendsto f (x₁ ⊔ x₂) y ↔ Tendsto f x₁ y ∧ Tendsto f x₂ y

theorem Filter.Tendsto.sup {α : Type u_1} {β : Type u_2} {f : α → β} {x₁ x₂ : Filter α} {y : Filter β} : Tendsto f x₁ y → Tendsto f x₂ y → Tendsto f (x₁ ⊔ x₂) y

theorem Filter.Tendsto.sup_sup {α : Type u_1} {β : Type u_2} {f : α → β} {x₁ x₂ : Filter α} {y₁ y₂ : Filter β} (h₁ : Tendsto f x₁ y₁) (h₂ : Tendsto f x₂ y₂) : 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 β} : Tendsto f (⨆ (i : ι), x i) y ↔ ∀ (i : ι), 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 : ι), Tendsto f (x i) (y i)) : Tendsto f (iSup x) (iSup y)

@[simp]

theorem Filter.tendsto_principal {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter α} {s : Set β} : Tendsto f l (principal s) ↔ ∀ᶠ (a : α) in l, f a ∈ s

theorem Filter.tendsto_principal_principal {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β} : Tendsto f (principal s) (principal t) ↔ ∀ a ∈ s, f a ∈ t

@[simp]

theorem Filter.tendsto_pure {α : Type u_1} {β : Type u_2} {f : α → β} {a : Filter α} {b : β} : Tendsto f a (pure b) ↔ ∀ᶠ (x : α) in a, f x = b

theorem Filter.tendsto_pure_pure {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : Tendsto f (pure a) (pure (f a))

theorem Filter.tendsto_const_pure {α : Type u_1} {β : Type u_2} {a : Filter α} {b : β} : Tendsto (fun (x : α) => b) a (pure b)

theorem Filter.pure_le_iff {α : Type u_1} {a : α} {l : Filter α} : pure a ≤ l ↔ ∀ s ∈ l, a ∈ s

theorem Filter.tendsto_pure_left {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} {l : 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 α} : map f (l ⊓ principal (f ⁻¹' s)) = map f l ⊓ principal s

theorem Filter.Tendsto.not_tendsto {α : Type u_1} {β : Type u_2} {f : α → β} {a : Filter α} {b₁ b₂ : Filter β} (hf : Tendsto f a b₁) [a.NeBot] (hb : Disjoint b₁ b₂) : ¬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₀ : Tendsto f (l₁ ⊓ principal {x : α | p x}) l₂) (h₁ : Tendsto g (l₁ ⊓ principal {x : α | ¬p x}) l₂) : 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 : Tendsto f l₁ l₂) (hg : Tendsto g l₁ l₂) : 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₀ : Tendsto f (l₁ ⊓ principal s) l₂) (h₁ : Tendsto g (l₁ ⊓ principal sᶜ) l₂) : Tendsto (s.piecewise f g) l₁ l₂

theorem Set.MapsTo.tendsto {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : MapsTo f s t) : Filter.Tendsto f (Filter.principal s) (Filter.principal t)

theorem Filter.EventuallyEq.comp_tendsto {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {f f' : α → β} (H : f =ᶠ[l] f') {g : γ → α} {lc : Filter γ} (hg : Tendsto g lc l) : f ∘ g =ᶠ[lc] f' ∘ g

theorem Filter.map_mapsTo_Iic_iff_tendsto {α : Type u_1} {β : Type u_2} {F : Filter α} {G : Filter β} {m : α → β} : Set.MapsTo (map m) (Set.Iic F) (Set.Iic G) ↔ Tendsto m F G

theorem Filter.Tendsto.map_mapsTo_Iic {α : Type u_1} {β : Type u_2} {F : Filter α} {G : Filter β} {m : α → β} : Tendsto m F G → Set.MapsTo (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 (map m) (Set.Iic (principal s)) (Set.Iic (principal t)) ↔ Set.MapsTo m s t

theorem Set.MapsTo.filter_map_Iic {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {m : α → β} : MapsTo m s t → MapsTo (Filter.map m) (Iic (Filter.principal s)) (Iic (Filter.principal t))

Alias of the reverse direction of Filter.map_mapsTo_Iic_iff_mapsTo.