Loogle!
Result
Found 1988 declarations mentioning nhds and Filter.Tendsto. Of these, 1954 match your pattern(s). Of these, only the first 200 are shown.
- limUnder_of_not_tendsto 📋 Mathlib.Topology.Basic
{X : Type u} {α : Type u_1} [TopologicalSpace X] [hX : Nonempty X] {f : Filter α} {g : α → X} (h : ¬∃ x, Filter.Tendsto g f (nhds x)) : limUnder f g = Classical.choice hX - tendsto_nhds_limUnder 📋 Mathlib.Topology.Basic
{X : Type u} {α : Type u_1} [TopologicalSpace X] {f : Filter α} {g : α → X} (h : ∃ x, Filter.Tendsto g f (nhds x)) : Filter.Tendsto g f (nhds (limUnder f g)) - tendsto_const_nhds 📋 Mathlib.Topology.Neighborhoods
{X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {f : Filter α} : Filter.Tendsto (fun x_1 => x) f (nhds x) - tendsto_pure_nhds 📋 Mathlib.Topology.Neighborhoods
{X : Type u} [TopologicalSpace X] {α : Type u_1} (f : α → X) (a : α) : Filter.Tendsto f (pure a) (nhds (f a)) - Filter.EventuallyEq.tendsto 📋 Mathlib.Topology.Neighborhoods
{X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {l : Filter α} {f : α → X} (hf : f =ᶠ[l] fun x_1 => x) : Filter.Tendsto f l (nhds x) - tendsto_nhds_of_eventually_eq 📋 Mathlib.Topology.Neighborhoods
{X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {l : Filter α} {f : α → X} (h : ∀ᶠ (x' : α) in l, f x' = x) : Filter.Tendsto f l (nhds x) - tendsto_atBot_of_eventually_const 📋 Mathlib.Topology.Neighborhoods
{X : Type u} [TopologicalSpace X] {x : X} {ι : Type u_2} [Preorder ι] {u : ι → X} {i₀ : ι} (h : ∀ i ≤ i₀, u i = x) : Filter.Tendsto u Filter.atBot (nhds x) - tendsto_atTop_of_eventually_const 📋 Mathlib.Topology.Neighborhoods
{X : Type u} [TopologicalSpace X] {x : X} {ι : Type u_2} [Preorder ι] {u : ι → X} {i₀ : ι} (h : ∀ i ≥ i₀, u i = x) : Filter.Tendsto u Filter.atTop (nhds x) - OrderTop.tendsto_atTop_nhds 📋 Mathlib.Topology.Neighborhoods
{X : Type u} [TopologicalSpace X] {α : Type u_1} [PartialOrder α] [OrderTop α] (f : α → X) : Filter.Tendsto f Filter.atTop (nhds (f ⊤)) - mem_closure_of_frequently_of_tendsto 📋 Mathlib.Topology.Neighborhoods
{X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {s : Set X} {f : α → X} {b : Filter α} (h : ∃ᶠ (x : α) in b, f x ∈ s) (hf : Filter.Tendsto f b (nhds x)) : x ∈ closure s - IsClosed.mem_of_frequently_of_tendsto 📋 Mathlib.Topology.Neighborhoods
{X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {s : Set X} {f : α → X} {b : Filter α} (hs : IsClosed s) (h : ∃ᶠ (x : α) in b, f x ∈ s) (hf : Filter.Tendsto f b (nhds x)) : x ∈ s - tendsto_nhds 📋 Mathlib.Topology.Neighborhoods
{X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {f : α → X} {l : Filter α} : Filter.Tendsto f l (nhds x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → f ⁻¹' s ∈ l - mem_closure_of_tendsto 📋 Mathlib.Topology.Neighborhoods
{X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {s : Set X} {f : α → X} {b : Filter α} [b.NeBot] (hf : Filter.Tendsto f b (nhds x)) (h : ∀ᶠ (x : α) in b, f x ∈ s) : x ∈ closure s - IsClosed.mem_of_tendsto 📋 Mathlib.Topology.Neighborhoods
{X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {s : Set X} {f : α → X} {b : Filter α} [b.NeBot] (hs : IsClosed s) (hf : Filter.Tendsto f b (nhds x)) (h : ∀ᶠ (x : α) in b, f x ∈ s) : x ∈ s - tendsto_inf_principal_nhds_iff_of_forall_eq 📋 Mathlib.Topology.Neighborhoods
{X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {f : α → X} {l : Filter α} {s : Set α} (h : ∀ a ∉ s, f a = x) : Filter.Tendsto f (l ⊓ Filter.principal s) (nhds x) ↔ Filter.Tendsto f l (nhds x) - tendsto_atTop_nhds 📋 Mathlib.Topology.Neighborhoods
{X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} [Nonempty α] [SemilatticeSup α] {f : α → X} : Filter.Tendsto f Filter.atTop (nhds x) ↔ ∀ (U : Set X), x ∈ U → IsOpen U → ∃ N, ∀ (n : α), N ≤ n → f n ∈ U - Filter.Tendsto.mapClusterPt 📋 Mathlib.Topology.ClusterPt
{X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} [F.NeBot] (h : Filter.Tendsto u F (nhds x)) : MapClusterPt x F u - MapClusterPt.tendsto_comp 📋 Mathlib.Topology.ClusterPt
{X : Type u} [TopologicalSpace X] {Y : Type v} {α : Type u_1} {F : Filter α} {u : α → X} {x : X} [TopologicalSpace Y] {f : X → Y} {y : Y} (hf : Filter.Tendsto f (nhds x) (nhds y)) (hu : MapClusterPt x F u) : MapClusterPt y F (f ∘ u) - MapClusterPt.tendsto_comp' 📋 Mathlib.Topology.ClusterPt
{X : Type u} [TopologicalSpace X] {Y : Type v} {α : Type u_1} {F : Filter α} {u : α → X} {x : X} [TopologicalSpace Y] {f : X → Y} {y : Y} (hf : Filter.Tendsto f (nhds x ⊓ Filter.map u F) (nhds y)) (hu : MapClusterPt x F u) : MapClusterPt y F (f ∘ u) - Continuous.tendsto 📋 Mathlib.Topology.Continuous
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) (x : X) : Filter.Tendsto f (nhds x) (nhds (f x)) - ContinuousAt.tendsto 📋 Mathlib.Topology.Continuous
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} (h : ContinuousAt f x) : Filter.Tendsto f (nhds x) (nhds (f x)) - Continuous.tendsto' 📋 Mathlib.Topology.Continuous
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) (x : X) (y : Y) (h : f x = y) : Filter.Tendsto f (nhds x) (nhds y) - tendsto_nhds_true 📋 Mathlib.Topology.Order
{α : Type u_1} {l : Filter α} {p : α → Prop} : Filter.Tendsto p l (nhds True) ↔ ∀ᶠ (x : α) in l, p x - tendsto_nhds_Prop 📋 Mathlib.Topology.Order
{α : Type u_1} {l : Filter α} {p : α → Prop} {q : Prop} : Filter.Tendsto p l (nhds q) ↔ q → ∀ᶠ (x : α) in l, p x - continuous_nhdsAdjoint_dom 📋 Mathlib.Topology.Order
{α : Type u} {β : Type v} [TopologicalSpace β] {f : α → β} {a : α} {l : Filter α} : Continuous f ↔ Filter.Tendsto f l (nhds (f a)) - TopologicalSpace.tendsto_nhds_generateFrom_iff 📋 Mathlib.Topology.Order
{α : Type u} {β : Type u_1} {m : α → β} {f : Filter α} {g : Set (Set β)} {b : β} : Filter.Tendsto m f (nhds b) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f - Topology.IsClosedEmbedding.tendsto_nhds_iff 📋 Mathlib.Topology.Maps.Basic
{X : Type u_1} {Y : Type u_2} {ι : Type u_4} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] {g : ι → X} {l : Filter ι} {x : X} (hf : Topology.IsClosedEmbedding f) : Filter.Tendsto g l (nhds x) ↔ Filter.Tendsto (f ∘ g) l (nhds (f x)) - Topology.IsEmbedding.tendsto_nhds_iff 📋 Mathlib.Topology.Maps.Basic
{Y : Type u_2} {Z : Type u_3} {ι : Type u_4} {g : Y → Z} [TopologicalSpace Y] [TopologicalSpace Z] {f : ι → Y} {l : Filter ι} {y : Y} (hg : Topology.IsEmbedding g) : Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (g ∘ f) l (nhds (g y)) - Topology.IsInducing.tendsto_nhds_iff 📋 Mathlib.Topology.Maps.Basic
{Y : Type u_2} {Z : Type u_3} {ι : Type u_4} {g : Y → Z} [TopologicalSpace Y] [TopologicalSpace Z] {f : ι → Y} {l : Filter ι} {y : Y} (hg : Topology.IsInducing g) : Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (g ∘ f) l (nhds (g y)) - Topology.IsOpenEmbedding.tendsto_nhds_iff 📋 Mathlib.Topology.Maps.Basic
{Y : Type u_2} {Z : Type u_3} {ι : Type u_4} {g : Y → Z} [TopologicalSpace Y] [TopologicalSpace Z] {f : ι → Y} {l : Filter ι} {y : Y} (hg : Topology.IsOpenEmbedding g) : Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (g ∘ f) l (nhds (g y)) - Filter.Tendsto.fst_nhds 📋 Mathlib.Topology.Constructions.SumProd
{Y : Type v} {Z : Type u_2} [TopologicalSpace Y] [TopologicalSpace Z] {X : Type u_5} {l : Filter X} {f : X → Y × Z} {p : Y × Z} (h : Filter.Tendsto f l (nhds p)) : Filter.Tendsto (fun a => (f a).1) l (nhds p.1) - Filter.Tendsto.snd_nhds 📋 Mathlib.Topology.Constructions.SumProd
{Y : Type v} {Z : Type u_2} [TopologicalSpace Y] [TopologicalSpace Z] {X : Type u_5} {l : Filter X} {f : X → Y × Z} {p : Y × Z} (h : Filter.Tendsto f l (nhds p)) : Filter.Tendsto (fun a => (f a).2) l (nhds p.2) - Filter.Tendsto.prodMk_nhds 📋 Mathlib.Topology.Constructions.SumProd
{X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {γ : Type u_5} {x : X} {y : Y} {f : Filter γ} {mx : γ → X} {my : γ → Y} (hx : Filter.Tendsto mx f (nhds x)) (hy : Filter.Tendsto my f (nhds y)) : Filter.Tendsto (fun c => (mx c, my c)) f (nhds (x, y)) - Prod.tendsto_iff 📋 Mathlib.Topology.Constructions.SumProd
{Y : Type v} {Z : Type u_2} [TopologicalSpace Y] [TopologicalSpace Z] {X : Type u_5} (seq : X → Y × Z) {f : Filter X} (p : Y × Z) : Filter.Tendsto seq f (nhds p) ↔ Filter.Tendsto (fun n => (seq n).1) f (nhds p.1) ∧ Filter.Tendsto (fun n => (seq n).2) f (nhds p.2) - Filter.Tendsto.prodMap_nhds 📋 Mathlib.Topology.Constructions.SumProd
{X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {x : X} {y : Y} {z : Z} {w : W} {f : X → Y} {g : Z → W} (hf : Filter.Tendsto f (nhds x) (nhds y)) (hg : Filter.Tendsto g (nhds z) (nhds w)) : Filter.Tendsto (Prod.map f g) (nhds (x, z)) (nhds (y, w)) - tendsto_subtype_rng 📋 Mathlib.Topology.Constructions
{X : Type u} [TopologicalSpace X] {Y : Type u_5} {p : X → Prop} {l : Filter Y} {f : Y → Subtype p} {x : Subtype p} : Filter.Tendsto f l (nhds x) ↔ Filter.Tendsto (fun x => ↑(f x)) l (nhds ↑x) - Filter.Tendsto.apply_nhds 📋 Mathlib.Topology.Constructions
{Y : Type v} {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {l : Filter Y} {f : Y → (i : ι) → A i} {x : (i : ι) → A i} (h : Filter.Tendsto f l (nhds x)) (i : ι) : Filter.Tendsto (fun a => f a i) l (nhds (x i)) - tendsto_pi_nhds 📋 Mathlib.Topology.Constructions
{Y : Type v} {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {f : Y → (i : ι) → A i} {g : (i : ι) → A i} {u : Filter Y} : Filter.Tendsto f u (nhds g) ↔ ∀ (x : ι), Filter.Tendsto (fun i => f i x) u (nhds (g x)) - Filter.Tendsto.matrixVecCons 📋 Mathlib.Topology.Constructions
{Y : Type v} {Z : Type u_1} [TopologicalSpace Z] {n : ℕ} {f : Y → Z} {g : Y → Fin n → Z} {l : Filter Y} {x : Z} {y : Fin n → Z} (hf : Filter.Tendsto f l (nhds x)) (hg : Filter.Tendsto g l (nhds y)) : Filter.Tendsto (fun a => Matrix.vecCons (f a) (g a)) l (nhds (Matrix.vecCons x y)) - Filter.Tendsto.update 📋 Mathlib.Topology.Constructions
{Y : Type v} {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] [DecidableEq ι] {l : Filter Y} {f : Y → (i : ι) → A i} {x : (i : ι) → A i} (hf : Filter.Tendsto f l (nhds x)) (i : ι) {g : Y → A i} {xi : A i} (hg : Filter.Tendsto g l (nhds xi)) : Filter.Tendsto (fun a => Function.update (f a) i (g a)) l (nhds (Function.update x i xi)) - Filter.Tendsto.finInit 📋 Mathlib.Topology.Constructions
{Y : Type v} {n : ℕ} {A : Fin (n + 1) → Type u_9} [(i : Fin (n + 1)) → TopologicalSpace (A i)] {f : Y → (j : Fin (n + 1)) → A j} {l : Filter Y} {x : (j : Fin (n + 1)) → A j} (hg : Filter.Tendsto f l (nhds x)) : Filter.Tendsto (fun a => Fin.init (f a)) l (nhds (Fin.init x)) - Filter.Tendsto.finTail 📋 Mathlib.Topology.Constructions
{Y : Type v} {n : ℕ} {A : Fin (n + 1) → Type u_9} [(i : Fin (n + 1)) → TopologicalSpace (A i)] {f : Y → (j : Fin (n + 1)) → A j} {l : Filter Y} {x : (j : Fin (n + 1)) → A j} (hg : Filter.Tendsto f l (nhds x)) : Filter.Tendsto (fun a => Fin.tail (f a)) l (nhds (Fin.tail x)) - Filter.Tendsto.finSnoc 📋 Mathlib.Topology.Constructions
{Y : Type v} {n : ℕ} {A : Fin (n + 1) → Type u_9} [(i : Fin (n + 1)) → TopologicalSpace (A i)] {f : Y → (j : Fin n) → A j.castSucc} {g : Y → A (Fin.last n)} {l : Filter Y} {x : (j : Fin n) → A j.castSucc} {y : A (Fin.last n)} (hf : Filter.Tendsto f l (nhds x)) (hg : Filter.Tendsto g l (nhds y)) : Filter.Tendsto (fun a => Fin.snoc (f a) (g a)) l (nhds (Fin.snoc x y)) - Filter.Tendsto.finInsertNth 📋 Mathlib.Topology.Constructions
{Y : Type v} {n : ℕ} {A : Fin (n + 1) → Type u_9} [(i : Fin (n + 1)) → TopologicalSpace (A i)] (i : Fin (n + 1)) {f : Y → A i} {g : Y → (j : Fin n) → A (i.succAbove j)} {l : Filter Y} {x : A i} {y : (j : Fin n) → A (i.succAbove j)} (hf : Filter.Tendsto f l (nhds x)) (hg : Filter.Tendsto g l (nhds y)) : Filter.Tendsto (fun a => i.insertNth (f a) (g a)) l (nhds (i.insertNth x y)) - Filter.Tendsto.finCons 📋 Mathlib.Topology.Constructions
{Y : Type v} {n : ℕ} {A : Fin (n + 1) → Type u_9} [(i : Fin (n + 1)) → TopologicalSpace (A i)] {f : Y → A 0} {g : Y → (j : Fin n) → A j.succ} {l : Filter Y} {x : A 0} {y : (j : Fin n) → A j.succ} (hf : Filter.Tendsto f l (nhds x)) (hg : Filter.Tendsto g l (nhds y)) : Filter.Tendsto (fun a => Fin.cons (f a) (g a)) l (nhds (Fin.cons x y)) - tendsto_nhds_of_tendsto_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
{α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : β → α} {a : α} {s : Set α} {l : Filter β} (h : Filter.Tendsto f l (nhdsWithin a s)) : Filter.Tendsto f l (nhds a) - tendsto_nhdsWithin_range 📋 Mathlib.Topology.NhdsWithin
{α : Type u_1} {β : Type u_2} [TopologicalSpace α] {a : α} {l : Filter β} {f : β → α} : Filter.Tendsto f l (nhdsWithin a (Set.range f)) ↔ Filter.Tendsto f l (nhds a) - continuousAt_iff_punctured_nhds 📋 Mathlib.Topology.NhdsWithin
{α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {a : α} : ContinuousAt f a ↔ Filter.Tendsto f (nhdsWithin a {a}ᶜ) (nhds (f a)) - tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within 📋 Mathlib.Topology.NhdsWithin
{α : Type u_1} {β : Type u_2} [TopologicalSpace α] {a : α} {l : Filter β} {s : Set α} (f : β → α) (h1 : Filter.Tendsto f l (nhds a)) (h2 : ∀ᶠ (x : β) in l, f x ∈ s) : Filter.Tendsto f l (nhdsWithin a s) - tendsto_nhdsWithin_iff 📋 Mathlib.Topology.NhdsWithin
{α : Type u_1} {β : Type u_2} [TopologicalSpace α] {a : α} {l : Filter β} {s : Set α} {f : β → α} : Filter.Tendsto f l (nhdsWithin a s) ↔ Filter.Tendsto f l (nhds a) ∧ ∀ᶠ (n : β) in l, f n ∈ s - TopologicalSpace.FirstCountableTopology.tendsto_subseq 📋 Mathlib.Topology.Bases
{α : Type u} [t : TopologicalSpace α] [FirstCountableTopology α] {u : ℕ → α} {x : α} (hx : MapClusterPt x Filter.atTop u) : ∃ ψ, StrictMono ψ ∧ Filter.Tendsto (u ∘ ψ) Filter.atTop (nhds x) - ContinuousWithinAt.tendsto 📋 Mathlib.Topology.ContinuousOn
{α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) : Filter.Tendsto f (nhdsWithin x s) (nhds (f x)) - Continuous.tendsto_nhdsSet_nhds 📋 Mathlib.Topology.ContinuousOn
{α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {b : β} {f : α → β} (h : Continuous f) (h' : Set.EqOn f (fun x => b) s) : Filter.Tendsto f (nhdsSet s) (nhds b) - continuous_iff_ultrafilter 📋 Mathlib.Topology.Ultrafilter
{X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : Continuous f ↔ ∀ (x : X) (g : Ultrafilter X), ↑g ≤ nhds x → Filter.Tendsto f (↑g) (nhds (f x)) - continuousAt_iff_ultrafilter 📋 Mathlib.Topology.Ultrafilter
{X : Type u} {Y : Type v} {x : X} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : ContinuousAt f x ↔ ∀ (g : Ultrafilter X), ↑g ≤ nhds x → Filter.Tendsto f (↑g) (nhds (f x)) - mapClusterPt_iff_ultrafilter 📋 Mathlib.Topology.Ultrafilter
{X : Type u} {α : Type u_1} {x : X} [TopologicalSpace X] {F : Filter α} {u : α → X} : MapClusterPt x F u ↔ ∃ U, ↑U ≤ F ∧ Filter.Tendsto u (↑U) (nhds x) - Filter.Tendsto.isCompact_insert_range 📋 Mathlib.Topology.Compactness.Compact
{X : Type u} [TopologicalSpace X] {f : ℕ → X} {x : X} (hf : Filter.Tendsto f Filter.atTop (nhds x)) : IsCompact (insert x (Set.range f)) - Filter.Tendsto.isCompact_insert_range_of_cofinite 📋 Mathlib.Topology.Compactness.Compact
{X : Type u} {ι : Type u_1} [TopologicalSpace X] {f : ι → X} {x : X} (hf : Filter.Tendsto f Filter.cofinite (nhds x)) : IsCompact (insert x (Set.range f)) - tendsto_nhds_of_unique_mapClusterPt 📋 Mathlib.Topology.Compactness.Compact
{X : Type u} [TopologicalSpace X] [CompactSpace X] {Y : Type u_2} {l : Filter Y} {y : X} {f : Y → X} (h : ∀ (x : X), MapClusterPt x l f → x = y) : Filter.Tendsto f l (nhds y) - Filter.Tendsto.isCompact_insert_range_of_cocompact 📋 Mathlib.Topology.Compactness.Compact
{X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {y : Y} (hf : Filter.Tendsto f (Filter.cocompact X) (nhds y)) (hfc : Continuous f) : IsCompact (insert y (Set.range f)) - IsCompact.tendsto_nhds_of_unique_mapClusterPt 📋 Mathlib.Topology.Compactness.Compact
{X : Type u} [TopologicalSpace X] {s : Set X} {Y : Type u_2} {l : Filter Y} {y : X} {f : Y → X} (hs : IsCompact s) (hmem : ∀ᶠ (x : Y) in l, f x ∈ s) (h : ∀ x ∈ s, MapClusterPt x l f → x = y) : Filter.Tendsto f l (nhds y) - continuousAt_update_same 📋 Mathlib.Topology.Piecewise
{α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} [DecidableEq α] {y : β} : ContinuousAt (Function.update f x y) x ↔ Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds y) - continuousWithinAt_update_same 📋 Mathlib.Topology.Piecewise
{α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} [DecidableEq α] {y : β} : ContinuousWithinAt (Function.update f x y) s x ↔ Filter.Tendsto f (nhdsWithin x (s \ {x})) (nhds y) - continuous_if' 📋 Mathlib.Topology.Piecewise
{α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {p : α → Prop} [(a : α) → Decidable (p a)] (hpf : ∀ a ∈ frontier {x | p x}, Filter.Tendsto f (nhdsWithin a {x | p x}) (nhds (if p a then f a else g a))) (hpg : ∀ a ∈ frontier {x | p x}, Filter.Tendsto g (nhdsWithin a {x | ¬p x}) (nhds (if p a then f a else g a))) (hf : ContinuousOn f {x | p x}) (hg : ContinuousOn g {x | ¬p x}) : Continuous fun a => if p a then f a else g a - ContinuousOn.piecewise' 📋 Mathlib.Topology.Piecewise
{α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {s t : Set α} [(a : α) → Decidable (a ∈ t)] (hpf : ∀ a ∈ s ∩ frontier t, Filter.Tendsto f (nhdsWithin a (s ∩ t)) (nhds (t.piecewise f g a))) (hpg : ∀ a ∈ s ∩ frontier t, Filter.Tendsto g (nhdsWithin a (s ∩ tᶜ)) (nhds (t.piecewise f g a))) (hf : ContinuousOn f (s ∩ t)) (hg : ContinuousOn g (s ∩ tᶜ)) : ContinuousOn (t.piecewise f g) s - ContinuousOn.if' 📋 Mathlib.Topology.Piecewise
{α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {p : α → Prop} {f g : α → β} [(a : α) → Decidable (p a)] (hpf : ∀ a ∈ s ∩ frontier {a | p a}, Filter.Tendsto f (nhdsWithin a (s ∩ {a | p a})) (nhds (if p a then f a else g a))) (hpg : ∀ a ∈ s ∩ frontier {a | p a}, Filter.Tendsto g (nhdsWithin a (s ∩ {a | ¬p a})) (nhds (if p a then f a else g a))) (hf : ContinuousOn f (s ∩ {a | p a})) (hg : ContinuousOn g (s ∩ {a | ¬p a})) : ContinuousOn (fun a => if p a then f a else g a) s - tendsto_const_nhds_iff 📋 Mathlib.Topology.Separation.Basic
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T1Space X] {l : Filter Y} [l.NeBot] {c d : X} : Filter.Tendsto (fun x => c) l (nhds d) ↔ c = d - eq_of_tendsto_nhds 📋 Mathlib.Topology.Separation.Basic
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {f : X → Y} {x : X} {y : Y} (h : Filter.Tendsto f (nhds x) (nhds y)) : f x = y - continuousAt_of_tendsto_nhds 📋 Mathlib.Topology.Separation.Basic
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {f : X → Y} {x : X} {y : Y} (h : Filter.Tendsto f (nhds x) (nhds y)) : ContinuousAt f x - Filter.Tendsto.eventually_ne 📋 Mathlib.Topology.Separation.Basic
{Y : Type u_2} {X : Type u_3} [TopologicalSpace Y] [T1Space Y] {g : X → Y} {l : Filter X} {b₁ b₂ : Y} (hg : Filter.Tendsto g l (nhds b₁)) (hb : b₁ ≠ b₂) : ∀ᶠ (z : X) in l, g z ≠ b₂ - tendsto_nhds_unique_inseparable 📋 Mathlib.Topology.Separation.Basic
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R1Space X] {f : Y → X} {l : Filter Y} {a b : X} [l.NeBot] (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto f l (nhds b)) : Inseparable a b - continuousOn_update_iff 📋 Mathlib.Topology.Separation.Basic
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T1Space X] [DecidableEq X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {x : X} {y : Y} : ContinuousOn (Function.update f x y) s ↔ ContinuousOn f (s \ {x}) ∧ (x ∈ s → Filter.Tendsto f (nhdsWithin x (s \ {x})) (nhds y)) - Filter.Tendsto.limUnder_eq 📋 Mathlib.Topology.Separation.Hausdorff
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {x : X} {f : Filter Y} [f.NeBot] {g : Y → X} (h : Filter.Tendsto g f (nhds x)) : limUnder f g = x - tendsto_nhds_unique 📋 Mathlib.Topology.Separation.Hausdorff
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {f : Y → X} {l : Filter Y} {a b : X} [l.NeBot] (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto f l (nhds b)) : a = b - tendsto_nhds_unique' 📋 Mathlib.Topology.Separation.Hausdorff
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {f : Y → X} {l : Filter Y} {a b : X} : l.NeBot → ∀ (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto f l (nhds b)), a = b - tendsto_nhds_unique_of_eventuallyEq 📋 Mathlib.Topology.Separation.Hausdorff
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {f g : Y → X} {l : Filter Y} {a b : X} [l.NeBot] (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto g l (nhds b)) (hfg : f =ᶠ[l] g) : a = b - tendsto_nhds_unique_of_frequently_eq 📋 Mathlib.Topology.Separation.Hausdorff
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {f g : Y → X} {l : Filter Y} {a b : X} (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto g l (nhds b)) (hfg : ∃ᶠ (x : Y) in l, f x = g x) : a = b - Filter.limUnder_eq_iff 📋 Mathlib.Topology.Separation.Hausdorff
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {f : Filter Y} [f.NeBot] {g : Y → X} (h : ∃ x, Filter.Tendsto g f (nhds x)) {x : X} : limUnder f g = x ↔ Filter.Tendsto g f (nhds x) - Filter.Tendsto.add_const 📋 Mathlib.Topology.Algebra.Monoid.Defs
{M : Type u_1} [TopologicalSpace M] [Add M] [SeparatelyContinuousAdd M] {α : Type u_2} {f : α → M} {x : Filter α} {a : M} (b : M) (hf : Filter.Tendsto f x (nhds a)) : Filter.Tendsto (fun x => f x + b) x (nhds (a + b)) - Filter.Tendsto.const_add 📋 Mathlib.Topology.Algebra.Monoid.Defs
{M : Type u_1} [TopologicalSpace M] [Add M] [SeparatelyContinuousAdd M] {α : Type u_2} {f : α → M} {x : Filter α} {a : M} (b : M) (hf : Filter.Tendsto f x (nhds a)) : Filter.Tendsto (fun x => b + f x) x (nhds (b + a)) - Filter.Tendsto.const_mul 📋 Mathlib.Topology.Algebra.Monoid.Defs
{M : Type u_1} [TopologicalSpace M] [Mul M] [SeparatelyContinuousMul M] {α : Type u_2} {f : α → M} {x : Filter α} {a : M} (b : M) (hf : Filter.Tendsto f x (nhds a)) : Filter.Tendsto (fun x => b * f x) x (nhds (b * a)) - Filter.Tendsto.mul_const 📋 Mathlib.Topology.Algebra.Monoid.Defs
{M : Type u_1} [TopologicalSpace M] [Mul M] [SeparatelyContinuousMul M] {α : Type u_2} {f : α → M} {x : Filter α} {a : M} (b : M) (hf : Filter.Tendsto f x (nhds a)) : Filter.Tendsto (fun x => f x * b) x (nhds (a * b)) - Filter.Tendsto.add 📋 Mathlib.Topology.Algebra.Monoid.Defs
{M : Type u_1} [TopologicalSpace M] [Add M] [ContinuousAdd M] {α : Type u_2} {f g : α → M} {x : Filter α} {a b : M} (hf : Filter.Tendsto f x (nhds a)) (hg : Filter.Tendsto g x (nhds b)) : Filter.Tendsto (fun x => f x + g x) x (nhds (a + b)) - Filter.Tendsto.mul 📋 Mathlib.Topology.Algebra.Monoid.Defs
{M : Type u_1} [TopologicalSpace M] [Mul M] [ContinuousMul M] {α : Type u_2} {f g : α → M} {x : Filter α} {a b : M} (hf : Filter.Tendsto f x (nhds a)) (hg : Filter.Tendsto g x (nhds b)) : Filter.Tendsto (fun x => f x * g x) x (nhds (a * b)) - Filter.tendsto_of_div_tendsto_one 📋 Mathlib.Topology.Algebra.Monoid.Defs
{α : Type u_2} {E : Type u_3} [CommGroup E] [TopologicalSpace E] [ContinuousMul E] {f g : α → E} (m : E) {x : Filter α} (hf : Filter.Tendsto f x (nhds m)) (hfg : Filter.Tendsto (g / f) x (nhds 1)) : Filter.Tendsto g x (nhds m) - Filter.tendsto_of_sub_tendsto_zero 📋 Mathlib.Topology.Algebra.Monoid.Defs
{α : Type u_2} {E : Type u_3} [AddCommGroup E] [TopologicalSpace E] [ContinuousAdd E] {f g : α → E} (m : E) {x : Filter α} (hf : Filter.Tendsto f x (nhds m)) (hfg : Filter.Tendsto (g - f) x (nhds 0)) : Filter.Tendsto g x (nhds m) - not_tendsto_atBot_of_tendsto_nhds 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [Preorder α] [NoBotOrder α] [TopologicalSpace α] [ClosedIicTopology α] {a : α} {l : Filter β} [l.NeBot] {f : β → α} (hf : Filter.Tendsto f l (nhds a)) : ¬Filter.Tendsto f l Filter.atBot - not_tendsto_atTop_of_tendsto_nhds 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [Preorder α] [NoTopOrder α] [TopologicalSpace α] [ClosedIciTopology α] {a : α} {l : Filter β} [l.NeBot] {f : β → α} (hf : Filter.Tendsto f l (nhds a)) : ¬Filter.Tendsto f l Filter.atTop - not_tendsto_nhds_of_tendsto_atBot 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [Preorder α] [NoBotOrder α] [TopologicalSpace α] [ClosedIicTopology α] {l : Filter β} [l.NeBot] {f : β → α} (hf : Filter.Tendsto f l Filter.atBot) (a : α) : ¬Filter.Tendsto f l (nhds a) - not_tendsto_nhds_of_tendsto_atTop 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [Preorder α] [NoTopOrder α] [TopologicalSpace α] [ClosedIciTopology α] {l : Filter β} [l.NeBot] {f : β → α} (hf : Filter.Tendsto f l Filter.atTop) (a : α) : ¬Filter.Tendsto f l (nhds a) - ge_of_tendsto' 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {f : β → α} {a b : α} {x : Filter β} [x.NeBot] (lim : Filter.Tendsto f x (nhds a)) (h : ∀ (c : β), b ≤ f c) : b ≤ a - ge_of_tendsto_of_frequently 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {f : β → α} {a b : α} {x : Filter β} (lim : Filter.Tendsto f x (nhds a)) (h : ∃ᶠ (c : β) in x, b ≤ f c) : b ≤ a - le_of_tendsto' 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {f : β → α} {a b : α} {x : Filter β} [x.NeBot] (lim : Filter.Tendsto f x (nhds a)) (h : ∀ (c : β), f c ≤ b) : a ≤ b - le_of_tendsto_of_frequently 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {f : β → α} {a b : α} {x : Filter β} (lim : Filter.Tendsto f x (nhds a)) (h : ∃ᶠ (c : β) in x, f c ≤ b) : a ≤ b - IsGLB.range_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {f : β → α} {a : α} {F : Filter β} [F.NeBot] (hle : ∀ (i : β), a ≤ f i) (hlim : Filter.Tendsto f F (nhds a)) : IsGLB (Set.range f) a - IsLUB.range_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {f : β → α} {a : α} {F : Filter β} [F.NeBot] (hle : ∀ (i : β), f i ≤ a) (hlim : Filter.Tendsto f F (nhds a)) : IsLUB (Set.range f) a - ge_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {f : β → α} {a b : α} {x : Filter β} [x.NeBot] (lim : Filter.Tendsto f x (nhds a)) (h : ∀ᶠ (c : β) in x, b ≤ f c) : b ≤ a - le_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {f : β → α} {a b : α} {x : Filter β} [x.NeBot] (lim : Filter.Tendsto f x (nhds a)) (h : ∀ᶠ (c : β) in x, f c ≤ b) : a ≤ b - le_of_tendsto_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {f g : β → α} {b : Filter β} {a₁ a₂ : α} [b.NeBot] (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) (h : f ≤ᶠ[b] g) : a₁ ≤ a₂ - tendsto_le_of_eventuallyLE 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {f g : β → α} {b : Filter β} {a₁ a₂ : α} [b.NeBot] (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) (h : f ≤ᶠ[b] g) : a₁ ≤ a₂ - le_of_tendsto_of_tendsto' 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {f g : β → α} {b : Filter β} {a₁ a₂ : α} [b.NeBot] (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) (h : ∀ (x : β), f x ≤ g x) : a₁ ≤ a₂ - le_of_tendsto_of_tendsto_of_frequently 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {f g : β → α} {b : Filter β} {a₁ a₂ : α} (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) (h : ∃ᶠ (x : β) in b, f x ≤ g x) : a₁ ≤ a₂ - Filter.Tendsto.max_left 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhds a)) : Filter.Tendsto (fun i => max (f i) a) l (nhds a) - Filter.Tendsto.max_right 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhds a)) : Filter.Tendsto (fun i => max a (f i)) l (nhds a) - Filter.Tendsto.min_left 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhds a)) : Filter.Tendsto (fun i => min (f i) a) l (nhds a) - Filter.Tendsto.min_right 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhds a)) : Filter.Tendsto (fun i => min a (f i)) l (nhds a) - iInf_eq_of_forall_le_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {ι : Type u_1} {F : Filter ι} [F.NeBot] [ConditionallyCompleteLattice α] [TopologicalSpace α] [ClosedIciTopology α] {a : α} {f : ι → α} (hle : ∀ (i : ι), a ≤ f i) (hlim : Filter.Tendsto f F (nhds a)) : ⨅ i, f i = a - iSup_eq_of_forall_le_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {ι : Type u_1} {F : Filter ι} [F.NeBot] [ConditionallyCompleteLattice α] [TopologicalSpace α] [ClosedIicTopology α] {a : α} {f : ι → α} (hle : ∀ (i : ι), f i ≤ a) (hlim : Filter.Tendsto f F (nhds a)) : ⨆ i, f i = a - Filter.Tendsto.eventually_const_le 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {l : Filter γ} {f : γ → α} {u v : α} (hv : u < v) (h : Filter.Tendsto f l (nhds v)) : ∀ᶠ (a : γ) in l, u ≤ f a - Filter.Tendsto.eventually_const_lt 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {l : Filter γ} {f : γ → α} {u v : α} (hv : u < v) (h : Filter.Tendsto f l (nhds v)) : ∀ᶠ (a : γ) in l, u < f a - Filter.Tendsto.eventually_le_const 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {l : Filter γ} {f : γ → α} {u v : α} (hv : v < u) (h : Filter.Tendsto f l (nhds v)) : ∀ᶠ (a : γ) in l, f a ≤ u - Filter.Tendsto.eventually_lt_const 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {l : Filter γ} {f : γ → α} {u v : α} (hv : v < u) (h : Filter.Tendsto f l (nhds v)) : ∀ᶠ (a : γ) in l, f a < u - Filter.Tendsto.max 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f g : β → α} {b : Filter β} {a₁ a₂ : α} (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) : Filter.Tendsto (fun b => max (f b) (g b)) b (nhds (max a₁ a₂)) - Filter.Tendsto.min 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f g : β → α} {b : Filter β} {a₁ a₂ : α} (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) : Filter.Tendsto (fun b => min (f b) (g b)) b (nhds (min a₁ a₂)) - Filter.Tendsto.eventually_lt 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {l : Filter γ} {f g : γ → α} {y z : α} (hf : Filter.Tendsto f l (nhds y)) (hg : Filter.Tendsto g l (nhds z)) (hyz : y < z) : ∀ᶠ (x : γ) in l, f x < g x - iUnion_Ici_eq_Ioi_of_lt_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {ι : Type u_1} {F : Filter ι} [F.NeBot] [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIciTopology α] {a : α} {f : ι → α} (hlt : ∀ (i : ι), a < f i) (hlim : Filter.Tendsto f F (nhds a)) : ⋃ i, Set.Ici (f i) = Set.Ioi a - iUnion_Iic_eq_Iio_of_lt_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
{α : Type u} {ι : Type u_1} {F : Filter ι} [F.NeBot] [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIicTopology α] {a : α} {f : ι → α} (hlt : ∀ (i : ι), f i < a) (hlim : Filter.Tendsto f F (nhds a)) : ⋃ i, Set.Iic (f i) = Set.Iio a - Tendsto.isLindelof_insert_range_of_coLindelof 📋 Mathlib.Topology.Compactness.Lindelof
{X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {y : Y} (hf : Filter.Tendsto f (Filter.coLindelof X) (nhds y)) (hfc : Continuous f) : IsLindelof (insert y (Set.range f)) - IsDenseInducing.tendsto_extend 📋 Mathlib.Topology.DenseEmbedding
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] (di : IsDenseInducing i) {f : α → γ} {a : α} (hf : ContinuousAt f a) : Filter.Tendsto f (nhds a) (nhds (di.extend f (i a))) - IsDenseInducing.extend_eq_at' 📋 Mathlib.Topology.DenseEmbedding
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] [T2Space γ] (di : IsDenseInducing i) {f : α → γ} {a : α} (c : γ) (hf : Filter.Tendsto f (nhds a) (nhds c)) : di.extend f (i a) = f a - IsDenseInducing.extend_eq_of_tendsto 📋 Mathlib.Topology.DenseEmbedding
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] [T2Space γ] (di : IsDenseInducing i) {b : β} {c : γ} {f : α → γ} (hf : Filter.Tendsto f (Filter.comap i (nhds b)) (nhds c)) : di.extend f b = c - IsDenseInducing.continuous_extend 📋 Mathlib.Topology.DenseEmbedding
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] [T3Space γ] {f : α → γ} (di : IsDenseInducing i) (hf : ∀ (b : β), ∃ c, Filter.Tendsto f (Filter.comap i (nhds b)) (nhds c)) : Continuous (di.extend f) - IsDenseInducing.extend_eq' 📋 Mathlib.Topology.DenseEmbedding
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] [T2Space γ] {f : α → γ} (di : IsDenseInducing i) (hf : ∀ (b : β), ∃ c, Filter.Tendsto f (Filter.comap i (nhds b)) (nhds c)) (a : α) : di.extend f (i a) = f a - Dense.extend_eq_of_tendsto 📋 Mathlib.Topology.DenseEmbedding
{α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : ↑s → β} [T2Space β] (hs : Dense s) {a : α} {b : β} (hf : Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds b)) : hs.extend f a = b - IsDenseInducing.continuousAt_extend 📋 Mathlib.Topology.DenseEmbedding
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] [T3Space γ] {b : β} {f : α → γ} (di : IsDenseInducing i) (hf : ∀ᶠ (x : β) in nhds b, ∃ c, Filter.Tendsto f (Filter.comap i (nhds x)) (nhds c)) : ContinuousAt (di.extend f) b - Dense.continuous_extend 📋 Mathlib.Topology.DenseEmbedding
{α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : ↑s → β} [T3Space β] (hs : Dense s) (hf : ∀ (a : α), ∃ b, Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds b)) : Continuous (hs.extend f) - IsDenseInducing.tendsto_comap_nhds_nhds 📋 Mathlib.Topology.DenseEmbedding
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace δ] {f : γ → α} {g : γ → δ} {h : δ → β} {d : δ} {a : α} (di : IsDenseInducing i) (H : Filter.Tendsto h (nhds d) (nhds (i a))) (comm : h ∘ g = i ∘ f) : Filter.Tendsto f (Filter.comap g (nhds d)) (nhds a) - Dense.continuousAt_extend 📋 Mathlib.Topology.DenseEmbedding
{α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : ↑s → β} [T3Space β] {a : α} (hs : Dense s) (hf : ∀ᶠ (x : α) in nhds a, ∃ b, Filter.Tendsto f (Filter.comap Subtype.val (nhds x)) (nhds b)) : ContinuousAt (hs.extend f) a - Uniform.tendsto_nhds_left 📋 Mathlib.Topology.UniformSpace.Basic
{α : Type ua} {β : Type ub} [UniformSpace α] {f : Filter β} {u : β → α} {a : α} : Filter.Tendsto u f (nhds a) ↔ Filter.Tendsto (fun x => (u x, a)) f (uniformity α) - Uniform.tendsto_nhds_right 📋 Mathlib.Topology.UniformSpace.Basic
{α : Type ua} {β : Type ub} [UniformSpace α] {f : Filter β} {u : β → α} {a : α} : Filter.Tendsto u f (nhds a) ↔ Filter.Tendsto (fun x => (a, u x)) f (uniformity α) - Filter.Tendsto.congr_uniformity 📋 Mathlib.Topology.UniformSpace.Basic
{α : Type u_2} {β : Type u_3} [UniformSpace β] {f g : α → β} {l : Filter α} {b : β} (hf : Filter.Tendsto f l (nhds b)) (hg : Filter.Tendsto (fun x => (f x, g x)) l (uniformity β)) : Filter.Tendsto g l (nhds b) - Uniform.tendsto_congr 📋 Mathlib.Topology.UniformSpace.Basic
{α : Type u_2} {β : Type u_3} [UniformSpace β] {f g : α → β} {l : Filter α} {b : β} (hfg : Filter.Tendsto (fun x => (f x, g x)) l (uniformity β)) : Filter.Tendsto f l (nhds b) ↔ Filter.Tendsto g l (nhds b) - tendsto_of_uniformContinuous_subtype 📋 Mathlib.Topology.UniformSpace.Basic
{α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α} {a : α} (hf : UniformContinuous fun x => f ↑x) (ha : s ∈ nhds a) : Filter.Tendsto f (nhds a) (nhds (f a)) - Filter.Tendsto.cauchy_map 📋 Mathlib.Topology.UniformSpace.Cauchy
{α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {l : Filter β} [l.NeBot] {f : β → α} {a : α} (h : Filter.Tendsto f l (nhds a)) : Cauchy (Filter.map f l) - cauchySeq_tendsto_of_complete 📋 Mathlib.Topology.UniformSpace.Cauchy
{α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] [CompleteSpace α] {u : β → α} (H : CauchySeq u) : ∃ x, Filter.Tendsto u Filter.atTop (nhds x) - cauchy_map_iff_exists_tendsto 📋 Mathlib.Topology.UniformSpace.Cauchy
{α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [CompleteSpace α] {l : Filter β} {f : β → α} [l.NeBot] : Cauchy (Filter.map f l) ↔ ∃ x, Filter.Tendsto f l (nhds x) - UniformSpace.complete_of_cauchySeq_tendsto 📋 Mathlib.Topology.UniformSpace.Cauchy
{α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] (H' : ∀ (u : ℕ → α), CauchySeq u → ∃ a, Filter.Tendsto u Filter.atTop (nhds a)) : CompleteSpace α - Filter.Tendsto.cauchySeq 📋 Mathlib.Topology.UniformSpace.Cauchy
{α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] [Nonempty β] {f : β → α} {x : α} (hx : Filter.Tendsto f Filter.atTop (nhds x)) : CauchySeq f - cauchySeq_tendsto_of_isComplete 📋 Mathlib.Topology.UniformSpace.Cauchy
{α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] {K : Set α} (h₁ : IsComplete K) {u : β → α} (h₂ : ∀ (n : β), u n ∈ K) (h₃ : CauchySeq u) : ∃ v ∈ K, Filter.Tendsto u Filter.atTop (nhds v) - tendsto_nhds_of_cauchySeq_of_subseq 📋 Mathlib.Topology.UniformSpace.Cauchy
{α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] {u : β → α} (hu : CauchySeq u) {ι : Type u_1} {f : ι → β} {p : Filter ι} [p.NeBot] (hf : Filter.Tendsto f p Filter.atTop) {a : α} (ha : Filter.Tendsto (u ∘ f) p (nhds a)) : Filter.Tendsto u Filter.atTop (nhds a) - UniformSpace.complete_of_convergent_controlled_sequences 📋 Mathlib.Topology.UniformSpace.Cauchy
{α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] (U : ℕ → SetRel α α) (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Filter.Tendsto u Filter.atTop (nhds a)) : CompleteSpace α - SequentiallyComplete.le_nhds_of_seq_tendsto_nhds 📋 Mathlib.Topology.UniformSpace.Cauchy
{α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (U_le : ∀ s ∈ uniformity α, ∃ n, U n ⊆ s) ⦃a : α⦄ (ha : Filter.Tendsto (SequentiallyComplete.seq hf U_mem) Filter.atTop (nhds a)) : f ≤ nhds a - CauchySeq.tendsto_limUnder 📋 Mathlib.Topology.UniformSpace.Cauchy
{α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] [CompleteSpace α] {u : β → α} (h : CauchySeq u) : Filter.Tendsto u Filter.atTop (nhds (limUnder Filter.atTop u)) - Filter.Tendsto.subseq_mem_entourage 📋 Mathlib.Topology.UniformSpace.Cauchy
{α : Type u} [uniformSpace : UniformSpace α] {V : ℕ → SetRel α α} (hV : ∀ (n : ℕ), V n ∈ uniformity α) {u : ℕ → α} {a : α} (hu : Filter.Tendsto u Filter.atTop (nhds a)) : ∃ φ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1) - Filter.Tendsto.inv 📋 Mathlib.Topology.Algebra.Group.Defs
{G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Inv G] [ContinuousInv G] {f : α → G} {l : Filter α} {y : G} (h : Filter.Tendsto f l (nhds y)) : Filter.Tendsto (fun x => (f x)⁻¹) l (nhds y⁻¹) - Filter.Tendsto.neg 📋 Mathlib.Topology.Algebra.Group.Defs
{G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {f : α → G} {l : Filter α} {y : G} (h : Filter.Tendsto f l (nhds y)) : Filter.Tendsto (fun x => -f x) l (nhds (-y)) - Filter.Tendsto.div' 📋 Mathlib.Topology.Algebra.Group.Defs
{G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Div G] [ContinuousDiv G] {f g : α → G} {l : Filter α} {a b : G} (hf : Filter.Tendsto f l (nhds a)) (hg : Filter.Tendsto g l (nhds b)) : Filter.Tendsto (fun x => f x / g x) l (nhds (a / b)) - Filter.Tendsto.sub 📋 Mathlib.Topology.Algebra.Group.Defs
{G : Type u_1} {α : Type u_2} [TopologicalSpace G] [Sub G] [ContinuousSub G] {f g : α → G} {l : Filter α} {a b : G} (hf : Filter.Tendsto f l (nhds a)) (hg : Filter.Tendsto g l (nhds b)) : Filter.Tendsto (fun x => f x - g x) l (nhds (a - b)) - HasCompactMulSupport.is_one_at_infty 📋 Mathlib.Topology.Algebra.Support
{α : Type u_2} {γ : Type u_5} [TopologicalSpace α] [One γ] {f : α → γ} [TopologicalSpace γ] (h : HasCompactMulSupport f) : Filter.Tendsto f (Filter.cocompact α) (nhds 1) - HasCompactSupport.is_zero_at_infty 📋 Mathlib.Topology.Algebra.Support
{α : Type u_2} {γ : Type u_5} [TopologicalSpace α] [Zero γ] {f : α → γ} [TopologicalSpace γ] (h : HasCompactSupport f) : Filter.Tendsto f (Filter.cocompact α) (nhds 0) - Filter.Tendsto.const_smul 📋 Mathlib.Topology.Algebra.ConstMulAction
{M : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] {f : β → α} {l : Filter β} {a : α} (hf : Filter.Tendsto f l (nhds a)) (c : M) : Filter.Tendsto (fun x => c • f x) l (nhds (c • a)) - Filter.Tendsto.const_vadd 📋 Mathlib.Topology.Algebra.ConstMulAction
{M : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] {f : β → α} {l : Filter β} {a : α} (hf : Filter.Tendsto f l (nhds a)) (c : M) : Filter.Tendsto (fun x => c +ᵥ f x) l (nhds (c +ᵥ a)) - IsUnit.tendsto_const_smul_iff 📋 Mathlib.Topology.Algebra.ConstMulAction
{M : Type u_1} {α : Type u_2} {β : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [ContinuousConstSMul M α] {f : β → α} {l : Filter β} {a : α} {c : M} (hc : IsUnit c) : Filter.Tendsto (fun x => c • f x) l (nhds (c • a)) ↔ Filter.Tendsto f l (nhds a) - tendsto_const_smul_iff 📋 Mathlib.Topology.Algebra.ConstMulAction
{α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] {f : β → α} {l : Filter β} {a : α} (c : G) : Filter.Tendsto (fun x => c • f x) l (nhds (c • a)) ↔ Filter.Tendsto f l (nhds a) - tendsto_const_vadd_iff 📋 Mathlib.Topology.Algebra.ConstMulAction
{α : Type u_2} {β : Type u_3} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] {f : β → α} {l : Filter β} {a : α} (c : G) : Filter.Tendsto (fun x => c +ᵥ f x) l (nhds (c +ᵥ a)) ↔ Filter.Tendsto f l (nhds a) - tendsto_const_smul_iff₀ 📋 Mathlib.Topology.Algebra.ConstMulAction
{α : Type u_2} {β : Type u_3} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] {f : β → α} {l : Filter β} {a : α} {c : G₀} (hc : c ≠ 0) : Filter.Tendsto (fun x => c • f x) l (nhds (c • a)) ↔ Filter.Tendsto f l (nhds a) - Filter.Tendsto.smul_const 📋 Mathlib.Topology.Algebra.MulAction
{M : Type u_1} {X : Type u_2} {α : Type u_4} [TopologicalSpace M] [TopologicalSpace X] [SMul M X] [ContinuousSMul M X] {f : α → M} {l : Filter α} {c : M} (hf : Filter.Tendsto f l (nhds c)) (a : X) : Filter.Tendsto (fun x => f x • a) l (nhds (c • a)) - Filter.Tendsto.vadd_const 📋 Mathlib.Topology.Algebra.MulAction
{M : Type u_1} {X : Type u_2} {α : Type u_4} [TopologicalSpace M] [TopologicalSpace X] [VAdd M X] [ContinuousVAdd M X] {f : α → M} {l : Filter α} {c : M} (hf : Filter.Tendsto f l (nhds c)) (a : X) : Filter.Tendsto (fun x => f x +ᵥ a) l (nhds (c +ᵥ a)) - Filter.Tendsto.smul 📋 Mathlib.Topology.Algebra.MulAction
{M : Type u_1} {X : Type u_2} {α : Type u_4} [TopologicalSpace M] [TopologicalSpace X] [SMul M X] [ContinuousSMul M X] {f : α → M} {g : α → X} {l : Filter α} {c : M} {a : X} (hf : Filter.Tendsto f l (nhds c)) (hg : Filter.Tendsto g l (nhds a)) : Filter.Tendsto (fun x => f x • g x) l (nhds (c • a)) - Filter.Tendsto.vadd 📋 Mathlib.Topology.Algebra.MulAction
{M : Type u_1} {X : Type u_2} {α : Type u_4} [TopologicalSpace M] [TopologicalSpace X] [VAdd M X] [ContinuousVAdd M X] {f : α → M} {g : α → X} {l : Filter α} {c : M} {a : X} (hf : Filter.Tendsto f l (nhds c)) (hg : Filter.Tendsto g l (nhds a)) : Filter.Tendsto (fun x => f x +ᵥ g x) l (nhds (c +ᵥ a)) - tendsto_add 📋 Mathlib.Topology.Algebra.Monoid
{M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] {a b : M} : Filter.Tendsto (fun p => p.1 + p.2) (nhds (a, b)) (nhds (a + b)) - tendsto_mul 📋 Mathlib.Topology.Algebra.Monoid
{M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] {a b : M} : Filter.Tendsto (fun p => p.1 * p.2) (nhds (a, b)) (nhds (a * b)) - Filter.Tendsto.nsmul 📋 Mathlib.Topology.Algebra.Monoid
{α : Type u_2} {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {l : Filter α} {f : α → M} {x : M} (hf : Filter.Tendsto f l (nhds x)) (n : ℕ) : Filter.Tendsto (fun x => n • f x) l (nhds (n • x)) - Filter.Tendsto.pow 📋 Mathlib.Topology.Algebra.Monoid
{α : Type u_2} {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] {l : Filter α} {f : α → M} {x : M} (hf : Filter.Tendsto f l (nhds x)) (n : ℕ) : Filter.Tendsto (fun x => f x ^ n) l (nhds (x ^ n)) - addHomOfTendsto 📋 Mathlib.Topology.Algebra.Monoid
{α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [Add M₁] [Add M₂] [ContinuousAdd M₂] {F : Type u_8} [FunLike F M₁ M₂] [AddHomClass F M₁ M₂] {l : Filter α} (f : M₁ → M₂) (g : α → F) [l.NeBot] (h : Filter.Tendsto (fun a x => (g a) x) l (nhds f)) : M₁ →ₙ+ M₂ - mulHomOfTendsto 📋 Mathlib.Topology.Algebra.Monoid
{α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [Mul M₁] [Mul M₂] [ContinuousMul M₂] {F : Type u_8} [FunLike F M₁ M₂] [MulHomClass F M₁ M₂] {l : Filter α} (f : M₁ → M₂) (g : α → F) [l.NeBot] (h : Filter.Tendsto (fun a x => (g a) x) l (nhds f)) : M₁ →ₙ* M₂ - Filter.Tendsto.addUnits 📋 Mathlib.Topology.Algebra.Monoid
{ι : Type u_1} {N : Type u_4} [TopologicalSpace N] [AddMonoid N] [ContinuousAdd N] [T2Space N] {f : ι → AddUnits N} {r₁ r₂ : N} {l : Filter ι} [l.NeBot] (h₁ : Filter.Tendsto (fun x => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun x => ↑(-f x)) l (nhds r₂)) : AddUnits N - Filter.Tendsto.units 📋 Mathlib.Topology.Algebra.Monoid
{ι : Type u_1} {N : Type u_4} [TopologicalSpace N] [Monoid N] [ContinuousMul N] [T2Space N] {f : ι → Nˣ} {r₁ r₂ : N} {l : Filter ι} [l.NeBot] (h₁ : Filter.Tendsto (fun x => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun x => ↑(f x)⁻¹) l (nhds r₂)) : Nˣ - tendsto_multiset_prod 📋 Mathlib.Topology.Algebra.Monoid
{ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Multiset ι) : (∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun b => (Multiset.map (fun c => f c b) s).prod) x (nhds (Multiset.map a s).prod) - tendsto_multiset_sum 📋 Mathlib.Topology.Algebra.Monoid
{ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Multiset ι) : (∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun b => (Multiset.map (fun c => f c b) s).sum) x (nhds (Multiset.map a s).sum) - tendsto_finset_prod 📋 Mathlib.Topology.Algebra.Monoid
{ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Finset ι) : (∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun b => ∏ c ∈ s, f c b) x (nhds (∏ c ∈ s, a c)) - tendsto_finset_sum 📋 Mathlib.Topology.Algebra.Monoid
{ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Finset ι) : (∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun b => ∑ c ∈ s, f c b) x (nhds (∑ c ∈ s, a c)) - addMonoidHomOfTendsto 📋 Mathlib.Topology.Algebra.Monoid
{α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [AddZeroClass M₁] [AddZeroClass M₂] [ContinuousAdd M₂] {F : Type u_8} [FunLike F M₁ M₂] [AddMonoidHomClass F M₁ M₂] {l : Filter α} (f : M₁ → M₂) (g : α → F) [l.NeBot] (h : Filter.Tendsto (fun a x => (g a) x) l (nhds f)) : M₁ →+ M₂ - monoidHomOfTendsto 📋 Mathlib.Topology.Algebra.Monoid
{α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [MulOneClass M₁] [MulOneClass M₂] [ContinuousMul M₂] {F : Type u_8} [FunLike F M₁ M₂] [MonoidHomClass F M₁ M₂] {l : Filter α} (f : M₁ → M₂) (g : α → F) [l.NeBot] (h : Filter.Tendsto (fun a x => (g a) x) l (nhds f)) : M₁ →* M₂ - Filter.Tendsto.val_addUnits 📋 Mathlib.Topology.Algebra.Monoid
{ι : Type u_1} {N : Type u_4} [TopologicalSpace N] [AddMonoid N] [ContinuousAdd N] [T2Space N] {f : ι → AddUnits N} {r₁ r₂ : N} {l : Filter ι} [l.NeBot] (h₁ : Filter.Tendsto (fun x => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun x => ↑(-f x)) l (nhds r₂)) : ↑(h₁.addUnits h₂) = r₁ - Filter.Tendsto.val_units 📋 Mathlib.Topology.Algebra.Monoid
{ι : Type u_1} {N : Type u_4} [TopologicalSpace N] [Monoid N] [ContinuousMul N] [T2Space N] {f : ι → Nˣ} {r₁ r₂ : N} {l : Filter ι} [l.NeBot] (h₁ : Filter.Tendsto (fun x => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun x => ↑(f x)⁻¹) l (nhds r₂)) : ↑(h₁.units h₂) = r₁ - Tendsto.tendsto_mul_zero_of_disjoint_cocompact_left 📋 Mathlib.Topology.Algebra.Monoid
{M : Type u_3} {α : Type u_6} [TopologicalSpace M] [MulZeroClass M] [ContinuousMul M] {f g : α → M} {l : Filter α} (hf : Disjoint (Filter.map f l) (Filter.cocompact M)) (hg : Filter.Tendsto g l (nhds 0)) : Filter.Tendsto (fun x => f x * g x) l (nhds 0) - Tendsto.tendsto_mul_zero_of_disjoint_cocompact_right 📋 Mathlib.Topology.Algebra.Monoid
{M : Type u_3} {α : Type u_6} [TopologicalSpace M] [MulZeroClass M] [ContinuousMul M] {f g : α → M} {l : Filter α} (hf : Filter.Tendsto f l (nhds 0)) (hg : Disjoint (Filter.map g l) (Filter.cocompact M)) : Filter.Tendsto (fun x => f x * g x) l (nhds 0) - Filter.Tendsto.val_inv_units 📋 Mathlib.Topology.Algebra.Monoid
{ι : Type u_1} {N : Type u_4} [TopologicalSpace N] [Monoid N] [ContinuousMul N] [T2Space N] {f : ι → Nˣ} {r₁ r₂ : N} {l : Filter ι} [l.NeBot] (h₁ : Filter.Tendsto (fun x => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun x => ↑(f x)⁻¹) l (nhds r₂)) : ↑(h₁.units h₂)⁻¹ = r₂ - Filter.Tendsto.val_neg_addUnits 📋 Mathlib.Topology.Algebra.Monoid
{ι : Type u_1} {N : Type u_4} [TopologicalSpace N] [AddMonoid N] [ContinuousAdd N] [T2Space N] {f : ι → AddUnits N} {r₁ r₂ : N} {l : Filter ι} [l.NeBot] (h₁ : Filter.Tendsto (fun x => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun x => ↑(-f x)) l (nhds r₂)) : ↑(-h₁.addUnits h₂) = r₂ - tendsto_mul_cofinite_nhds_zero 📋 Mathlib.Topology.Algebra.Monoid
{M : Type u_3} {α : Type u_6} {β : Type u_7} [TopologicalSpace M] [MulZeroClass M] [ContinuousMul M] {f : α → M} {g : β → M} (hf : Filter.Tendsto f Filter.cofinite (nhds 0)) (hg : Filter.Tendsto g Filter.cofinite (nhds 0)) : Filter.Tendsto (fun i => f i.1 * g i.2) Filter.cofinite (nhds 0) - addHomOfTendsto_apply 📋 Mathlib.Topology.Algebra.Monoid
{α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [Add M₁] [Add M₂] [ContinuousAdd M₂] {F : Type u_8} [FunLike F M₁ M₂] [AddHomClass F M₁ M₂] {l : Filter α} (f : M₁ → M₂) (g : α → F) [l.NeBot] (h : Filter.Tendsto (fun a x => (g a) x) l (nhds f)) : ⇑(addHomOfTendsto f g h) = f - mulHomOfTendsto_apply 📋 Mathlib.Topology.Algebra.Monoid
{α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [Mul M₁] [Mul M₂] [ContinuousMul M₂] {F : Type u_8} [FunLike F M₁ M₂] [MulHomClass F M₁ M₂] {l : Filter α} (f : M₁ → M₂) (g : α → F) [l.NeBot] (h : Filter.Tendsto (fun a x => (g a) x) l (nhds f)) : ⇑(mulHomOfTendsto f g h) = f - tendsto_mul_nhds_zero_prod_of_disjoint_cocompact 📋 Mathlib.Topology.Algebra.Monoid
{M : Type u_3} [TopologicalSpace M] [MulZeroClass M] [ContinuousMul M] {l : Filter M} (hl : Disjoint l (Filter.cocompact M)) : Filter.Tendsto (fun x => x.1 * x.2) (nhds 0 ×ˢ l) (nhds 0) - tendsto_mul_prod_nhds_zero_of_disjoint_cocompact 📋 Mathlib.Topology.Algebra.Monoid
{M : Type u_3} [TopologicalSpace M] [MulZeroClass M] [ContinuousMul M] {l : Filter M} (hl : Disjoint l (Filter.cocompact M)) : Filter.Tendsto (fun x => x.1 * x.2) (l ×ˢ nhds 0) (nhds 0) - tendsto_list_prod 📋 Mathlib.Topology.Algebra.Monoid
{ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [Monoid M] [ContinuousMul M] {f : ι → α → M} {x : Filter α} {a : ι → M} (l : List ι) : (∀ i ∈ l, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun b => (List.map (fun c => f c b) l).prod) x (nhds (List.map a l).prod) - tendsto_list_sum 📋 Mathlib.Topology.Algebra.Monoid
{ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] {f : ι → α → M} {x : Filter α} {a : ι → M} (l : List ι) : (∀ i ∈ l, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun b => (List.map (fun c => f c b) l).sum) x (nhds (List.map a l).sum) - addMonoidHomOfTendsto_apply 📋 Mathlib.Topology.Algebra.Monoid
{α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [AddZeroClass M₁] [AddZeroClass M₂] [ContinuousAdd M₂] {F : Type u_8} [FunLike F M₁ M₂] [AddMonoidHomClass F M₁ M₂] {l : Filter α} (f : M₁ → M₂) (g : α → F) [l.NeBot] (h : Filter.Tendsto (fun a x => (g a) x) l (nhds f)) : ⇑(addMonoidHomOfTendsto f g h) = f - monoidHomOfTendsto_apply 📋 Mathlib.Topology.Algebra.Monoid
{α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [TopologicalSpace M₂] [T2Space M₂] [MulOneClass M₁] [MulOneClass M₂] [ContinuousMul M₂] {F : Type u_8} [FunLike F M₁ M₂] [MonoidHomClass F M₁ M₂] {l : Filter α} (f : M₁ → M₂) (g : α → F) [l.NeBot] (h : Filter.Tendsto (fun a x => (g a) x) l (nhds f)) : ⇑(monoidHomOfTendsto f g h) = f - tendsto_mul_cocompact_nhds_zero 📋 Mathlib.Topology.Algebra.Monoid
{M : Type u_3} {α : Type u_6} {β : Type u_7} [TopologicalSpace M] [MulZeroClass M] [ContinuousMul M] [TopologicalSpace α] [TopologicalSpace β] {f : α → M} {g : β → M} (f_cont : Continuous f) (g_cont : Continuous g) (hf : Filter.Tendsto f (Filter.cocompact α) (nhds 0)) (hg : Filter.Tendsto g (Filter.cocompact β) (nhds 0)) : Filter.Tendsto (fun i => f i.1 * g i.2) (Filter.cocompact (α × β)) (nhds 0) - tendsto_mul_coprod_nhds_zero_inf_of_disjoint_cocompact 📋 Mathlib.Topology.Algebra.Monoid
{M : Type u_3} [TopologicalSpace M] [MulZeroClass M] [ContinuousMul M] {l : Filter (M × M)} (hl : Disjoint l (Filter.cocompact (M × M))) : Filter.Tendsto (fun x => x.1 * x.2) ((nhds 0).coprod (nhds 0) ⊓ l) (nhds 0) - tendsto_mul_nhds_zero_of_disjoint_cocompact 📋 Mathlib.Topology.Algebra.Monoid
{M : Type u_3} [TopologicalSpace M] [MulZeroClass M] [ContinuousMul M] {l : Filter (M × M)} (hl : Disjoint l (Filter.cocompact (M × M))) (h'l : l ≤ (nhds 0).coprod (nhds 0)) : Filter.Tendsto (fun x => x.1 * x.2) l (nhds 0) - continuousAdd_of_comm_of_nhds_zero 📋 Mathlib.Topology.Algebra.Monoid
(M : Type u) [AddCommMonoid M] [TopologicalSpace M] (hadd : Filter.Tendsto (Function.uncurry fun x1 x2 => x1 + x2) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hleft : ∀ (x₀ : M), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) : ContinuousAdd M - continuousMul_of_comm_of_nhds_one 📋 Mathlib.Topology.Algebra.Monoid
(M : Type u) [CommMonoid M] [TopologicalSpace M] (hmul : Filter.Tendsto (Function.uncurry fun x1 x2 => x1 * x2) (nhds 1 ×ˢ nhds 1) (nhds 1)) (hleft : ∀ (x₀ : M), nhds x₀ = Filter.map (fun x => x₀ * x) (nhds 1)) : ContinuousMul M - ContinuousAdd.of_nhds_zero 📋 Mathlib.Topology.Algebra.Monoid
{M : Type u} [AddMonoid M] [TopologicalSpace M] (hadd : Filter.Tendsto (Function.uncurry fun x1 x2 => x1 + x2) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hleft : ∀ (x₀ : M), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) (hright : ∀ (x₀ : M), nhds x₀ = Filter.map (fun x => x + x₀) (nhds 0)) : ContinuousAdd M - ContinuousMul.of_nhds_one 📋 Mathlib.Topology.Algebra.Monoid
{M : Type u} [Monoid M] [TopologicalSpace M] (hmul : Filter.Tendsto (Function.uncurry fun x1 x2 => x1 * x2) (nhds 1 ×ˢ nhds 1) (nhds 1)) (hleft : ∀ (x₀ : M), nhds x₀ = Filter.map (fun x => x₀ * x) (nhds 1)) (hright : ∀ (x₀ : M), nhds x₀ = Filter.map (fun x => x * x₀) (nhds 1)) : ContinuousMul M - tendsto_inv 📋 Mathlib.Topology.Algebra.Group.Basic
{G : Type w} [TopologicalSpace G] [Inv G] [ContinuousInv G] (a : G) : Filter.Tendsto Inv.inv (nhds a) (nhds a⁻¹) - tendsto_neg 📋 Mathlib.Topology.Algebra.Group.Basic
{G : Type w} [TopologicalSpace G] [Neg G] [ContinuousNeg G] (a : G) : Filter.Tendsto Neg.neg (nhds a) (nhds (-a)) - tendsto_inv_iff 📋 Mathlib.Topology.Algebra.Group.Basic
{G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {l : Filter α} {m : α → G} {a : G} : Filter.Tendsto (fun x => (m x)⁻¹) l (nhds a⁻¹) ↔ Filter.Tendsto m l (nhds a) - tendsto_neg_iff 📋 Mathlib.Topology.Algebra.Group.Basic
{G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] {l : Filter α} {m : α → G} {a : G} : Filter.Tendsto (fun x => -m x) l (nhds (-a)) ↔ Filter.Tendsto m l (nhds a)
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. You can also try the
#loogle command from LeanSearchClient,
the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"somewhere in their lemma name.By subexpression:
🔍_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
🔍Real.sqrt ?a * Real.sqrt ?aIf the pattern has parameters, they are matched in any order. Both of these will find
List.map:
🔍(?a -> ?b) -> List ?a -> List ?b
🔍List ?a -> (?a -> ?b) -> List ?bBy main conclusion:
🔍|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all→and∀) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍|- _ < _ → tsum _ < tsum _
will findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin
and tsum, have "two" as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _ (if
there were any such lemmas). Metavariables (?a) are
assigned independently in each filter.
The #lucky button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.
This is Loogle revision 401c76f serving mathlib revision b87935d