Loogle!

Result

Found 585 declarations mentioning Filter.Eventually and nhds. Of these, only the first 200 are shown.

• Filter.Eventually.self_of_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {p : X → Prop} (h : ∀ᶠ (y : X) in nhds x, p y) : p x
• isOpen_setOf_eventually_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {p : X → Prop} : IsOpen {x | ∀ᶠ (y : X) in nhds x, p y}
• 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)
• interior_setOf_eq 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {p : X → Prop} : interior {x | p x} = {x | ∀ᶠ (y : X) in nhds x, p y}
• Filter.Eventually.eventually_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {p : X → Prop} (h : ∀ᶠ (y : X) in nhds x, p y) : ∀ᶠ (y : X) in nhds x, ∀ᶠ (x : X) in nhds y, p x
• eventually_eventually_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {p : X → Prop} : (∀ᶠ (y : X) in nhds x, ∀ᶠ (x : X) in nhds y, p x) ↔ ∀ᶠ (x : X) in nhds x, p x
• IsOpen.eventually_mem 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} (hs : IsOpen s) (hx : x ∈ s) : ∀ᶠ (x : X) in nhds x, x ∈ s
• isOpen_iff_eventually 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsOpen s ↔ ∀ x ∈ s, ∀ᶠ (y : X) in nhds x, y ∈ s
• Filter.EventuallyEq.eventuallyEq_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {f g : X → α} (h : f =ᶠ[nhds x] g) : ∀ᶠ (y : X) in nhds x, f =ᶠ[nhds y] g
• eventually_eventuallyEq_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {f g : X → α} : (∀ᶠ (y : X) in nhds x, f =ᶠ[nhds y] g) ↔ f =ᶠ[nhds x] g
• eventually_mem_nhds_iff 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : (∀ᶠ (x' : X) in nhds x, s ∈ nhds x') ↔ s ∈ nhds x
• Filter.EventuallyLE.eventuallyLE_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} [LE α] {f g : X → α} (h : f ≤ᶠ[nhds x] g) : ∀ᶠ (y : X) in nhds x, f ≤ᶠ[nhds y] g
• eventually_eventuallyLE_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} [LE α] {f g : X → α} : (∀ᶠ (y : X) in nhds x, f ≤ᶠ[nhds y] g) ↔ f ≤ᶠ[nhds x] g
• eventually_nhds_iff 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {p : X → Prop} : (∀ᶠ (y : X) in nhds x, p y) ↔ ∃ t, (∀ y ∈ t, p y) ∧ IsOpen t ∧ x ∈ t
• 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
• ClusterPt.frequently 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} {p : X → Prop} (hx : ClusterPt x F) (hp : ∀ᶠ (y : X) in nhds x, p y) : ∃ᶠ (y : X) in F, p y
• MapClusterPt.frequently 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} (h : MapClusterPt x F u) {p : X → Prop} (hp : ∀ᶠ (y : X) in nhds x, p y) : ∃ᶠ (a : α) in F, p (u a)
• ContinuousAt.eventually_mem 📋 Mathlib.Topology.Continuous
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} (hf : ContinuousAt f x) {s : Set Y} (hs : s ∈ nhds (f x)) : ∀ᶠ (y : X) in nhds x, f y ∈ s
• 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
• TopologicalSpace.nhds_mkOfNhds 📋 Mathlib.Topology.Order
  {α : Type u} (n : α → Filter α) (a : α) (h₀ : pure ≤ n) (h₁ : ∀ (a : α), ∀ s ∈ n a, ∀ᶠ (y : α) in n a, s ∈ n y) : nhds a = n a
• TopologicalSpace.nhds_mkOfNhds_of_hasBasis 📋 Mathlib.Topology.Order
  {α : Type u} {n : α → Filter α} {ι : α → Sort u_1} {p : (a : α) → ι a → Prop} {s : (a : α) → ι a → Set α} (hb : ∀ (a : α), (n a).HasBasis (p a) (s a)) (hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i) (hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x) (a : α) : nhds a = n a
• Filter.Eventually.prod_inl_nhds 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {p : X → Prop} {x : X} (h : ∀ᶠ (x : X) in nhds x, p x) (y : Y) : ∀ᶠ (x : X × Y) in nhds (x, y), p x.1
• Filter.Eventually.prod_inr_nhds 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {p : Y → Prop} {y : Y} (h : ∀ᶠ (x : Y) in nhds y, p x) (x : X) : ∀ᶠ (x : X × Y) in nhds (x, y), p x.2
• Filter.Eventually.curry_nhds 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {p : X × Y → Prop} {x : X} {y : Y} (h : ∀ᶠ (x : X × Y) in nhds (x, y), p x) : ∀ᶠ (x' : X) in nhds x, ∀ᶠ (y' : Y) in nhds y, p (x', y')
• Filter.Eventually.prodMk_nhds 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {px : X → Prop} {x : X} (hx : ∀ᶠ (x : X) in nhds x, px x) {py : Y → Prop} {y : Y} (hy : ∀ᶠ (y : Y) in nhds y, py y) : ∀ᶠ (p : X × Y) in nhds (x, y), px p.1 ∧ py p.2
• Filter.Eventually.prod_mk_nhds 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {px : X → Prop} {x : X} (hx : ∀ᶠ (x : X) in nhds x, px x) {py : Y → Prop} {y : Y} (hy : ∀ᶠ (y : Y) in nhds y, py y) : ∀ᶠ (p : X × Y) in nhds (x, y), px p.1 ∧ py p.2
• Filter.Eventually.prod_nhds 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {p : X → Prop} {q : Y → Prop} {x : X} {y : Y} (hx : ∀ᶠ (x : X) in nhds x, p x) (hy : ∀ᶠ (y : Y) in nhds y, q y) : ∀ᶠ (z : X × Y) in nhds (x, y), p z.1 ∧ q z.2
• Filter.Eventually.eventually_nhdsSet 📋 Mathlib.Topology.NhdsSet
  {X : Type u_1} [TopologicalSpace X] {s : Set X} {p : X → Prop} (h : ∀ᶠ (y : X) in nhdsSet s, p y) : ∀ᶠ (y : X) in nhdsSet s, ∀ᶠ (x : X) in nhds y, p x
• eventually_nhdsSet_iff_forall 📋 Mathlib.Topology.NhdsSet
  {X : Type u_1} [TopologicalSpace X] {s : Set X} {p : X → Prop} : (∀ᶠ (x : X) in nhdsSet s, p x) ↔ ∀ x ∈ s, ∀ᶠ (y : X) in nhds x, p y
• map_nhds_subtype_coe_eq_nhds 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {p : X → Prop} {x : X} (hx : p x) (h : ∀ᶠ (x : X) in nhds x, p x) : Filter.map Subtype.val (nhds ⟨x, hx⟩) = nhds x
• Filter.eventually_nhdsSet_prod_iff 📋 Mathlib.Topology.Constructions
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} {p : X × Y → Prop} : (∀ᶠ (q : X × Y) in nhdsSet (s ×ˢ t), p q) ↔ ∀ x ∈ s, ∀ y ∈ t, ∃ px, (∀ᶠ (x' : X) in nhds x, px x') ∧ ∃ py, (∀ᶠ (y' : Y) in nhds y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)
• eventually_nhdsWithin_of_eventually_nhds 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} [TopologicalSpace α] {s : Set α} {a : α} {p : α → Prop} (h : ∀ᶠ (x : α) in nhds a, p x) : ∀ᶠ (x : α) in nhdsWithin a s, p x
• eventually_nhdsWithin_iff 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop} : (∀ᶠ (x : α) in nhdsWithin a s, p x) ↔ ∀ᶠ (x : α) in nhds a, x ∈ s → p x
• eventually_nhds_nhdsWithin 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop} : (∀ᶠ (y : α) in nhds a, ∀ᶠ (x : α) in nhdsWithin y s, p x) ↔ ∀ᶠ (x : α) in nhdsWithin a s, p x
• eventuallyEq_nhdsWithin_iff 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f g : α → β} {s : Set α} {a : α} : f =ᶠ[nhdsWithin a s] g ↔ ∀ᶠ (x : α) in nhds a, x ∈ s → f x = g x
• tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within 📋 Mathlib.Topology.ContinuousOn
  {α : 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)
• mem_nhdsWithin_iff_eventually 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} : t ∈ nhdsWithin x s ↔ ∀ᶠ (y : α) in nhds x, y ∈ s → y ∈ t
• tendsto_nhdsWithin_iff 📋 Mathlib.Topology.ContinuousOn
  {α : 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
• eventually_nhds_subtype_iff 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} [TopologicalSpace α] (s : Set α) (a : ↑s) (P : α → Prop) : (∀ᶠ (x : ↑s) in nhds a, P ↑x) ↔ ∀ᶠ (x : α) in nhdsWithin (↑a) s, P x
• 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)
• IsCompact.eventually_forall_of_forall_eventually 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x₀ : X} {K : Set Y} (hK : IsCompact K) {P : X → Y → Prop} (hP : ∀ y ∈ K, ∀ᶠ (z : X × Y) in nhds (x₀, y), P z.1 z.2) : ∀ᶠ (x : X) in nhds x₀, ∀ y ∈ K, P x y
• LocallyFinite.eventually_smallSets 📋 Mathlib.Topology.LocallyFinite
  {ι : Type u_1} {X : Type u_4} [TopologicalSpace X] {f : ι → Set X} (hf : LocallyFinite f) (x : X) : ∀ᶠ (s : Set X) in (nhds x).smallSets, {i | (f i ∩ s).Nonempty}.Finite
• locallyFinite_iff_smallSets 📋 Mathlib.Topology.LocallyFinite
  {ι : Type u_1} {X : Type u_4} [TopologicalSpace X] {f : ι → Set X} : LocallyFinite f ↔ ∀ (x : X), ∀ᶠ (s : Set X) in (nhds x).smallSets, {i | (f i ∩ s).Nonempty}.Finite
• LocallyFinite.eventually_subset 📋 Mathlib.Topology.LocallyFinite
  {ι : Type u_1} {X : Type u_4} [TopologicalSpace X] {s : ι → Set X} (hs : LocallyFinite s) (hs' : ∀ (i : ι), IsClosed (s i)) (x : X) : ∀ᶠ (y : X) in nhds x, {i | y ∈ s i} ⊆ {i | x ∈ s i}
• LocallyFinite.exists_forall_eventually_atTop_eventuallyEq 📋 Mathlib.Topology.LocallyFinite
  {α : Type u_3} {X : Type u_4} [TopologicalSpace X] {f : ℕ → X → α} (hf : LocallyFinite fun n => {x | f (n + 1) x ≠ f n x}) : ∃ F, ∀ (x : X), ∀ᶠ (n : ℕ) in Filter.atTop, f n =ᶠ[nhds x] F
• LocallyFinite.exists_forall_eventually_atTop_eventually_eq' 📋 Mathlib.Topology.LocallyFinite
  {X : Type u_4} [TopologicalSpace X] {π : X → Sort u_6} {f : ℕ → (x : X) → π x} (hf : LocallyFinite fun n => {x | f (n + 1) x ≠ f n x}) : ∃ F, ∀ (x : X), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ᶠ (y : X) in nhds x, f n y = F y
• LocallyFinite.exists_forall_eventually_eq_prod 📋 Mathlib.Topology.LocallyFinite
  {X : Type u_4} [TopologicalSpace X] {π : X → Sort u_6} {f : ℕ → (x : X) → π x} (hf : LocallyFinite fun n => {x | f (n + 1) x ≠ f n x}) : ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in Filter.atTop ×ˢ nhds x, f p.1 p.2 = F p.2
• eventually_ne_nhds 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] {a b : X} (h : a ≠ b) : ∀ᶠ (x : X) in nhds a, x ≠ b
• 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₂
• ContinuousAt.eventually_ne 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {g : X → Y} {x : X} {y : Y} (hg1 : ContinuousAt g x) (hg2 : g x ≠ y) : ∀ᶠ (z : X) in nhds x, g z ≠ y
• ContinuousAt.ne_iff_eventually_ne 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {x : X} {f g : X → Y} (hf : ContinuousAt f x) (hg : ContinuousAt g x) : f x ≠ g x ↔ ∀ᶠ (x : X) in nhds x, f x ≠ g x
• PreconnectedSpace.induction₂ 📋 Mathlib.Topology.Connected.Clopen
  {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] (P : α → α → Prop) (h : ∀ (x : α), ∀ᶠ (y : α) in nhds x, P x y) (h' : Transitive P) (h'' : Symmetric P) (x y : α) : P x y
• PreconnectedSpace.induction₂' 📋 Mathlib.Topology.Connected.Clopen
  {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] (P : α → α → Prop) (h : ∀ (x : α), ∀ᶠ (y : α) in nhds x, P x y ∧ P y x) (h' : Transitive P) (x y : α) : P x y
• 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
• IsDenseInducing.extend_unique_at 📋 Mathlib.Topology.DenseEmbedding
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [TopologicalSpace γ] [T2Space γ] {b : β} {f : α → γ} {g : β → γ} (di : IsDenseInducing i) (hf : ∀ᶠ (x : α) in Filter.comap i (nhds b), g (i x) = f x) (hg : ContinuousAt g b) : di.extend f b = g b
• 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
• Dense.extend_unique_at 📋 Mathlib.Topology.DenseEmbedding
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : ↑s → β} [T2Space β] {a : α} {g : α → β} (hs : Dense s) (hf : ∀ᶠ (x : ↑s) in Filter.comap Subtype.val (nhds a), g ↑x = f x) (hg : ContinuousAt g a) : hs.extend f a = g a
• LocallyFinite.exists_finset_mulSupport 📋 Mathlib.Topology.Algebra.Monoid
  {ι : Type u_1} {X : Type u_5} [TopologicalSpace X] {M : Type u_6} [One M] {f : ι → X → M} (hf : LocallyFinite fun i => Function.mulSupport (f i)) (x₀ : X) : ∃ I, ∀ᶠ (x : X) in nhds x₀, (Function.mulSupport fun i => f i x) ⊆ ↑I
• LocallyFinite.exists_finset_support 📋 Mathlib.Topology.Algebra.Monoid
  {ι : Type u_1} {X : Type u_5} [TopologicalSpace X] {M : Type u_6} [Zero M] {f : ι → X → M} (hf : LocallyFinite fun i => Function.support (f i)) (x₀ : X) : ∃ I, ∀ᶠ (x : X) in nhds x₀, (Function.support fun i => f i x) ⊆ ↑I
• finprod_eventually_eq_prod 📋 Mathlib.Topology.Algebra.Monoid
  {ι : Type u_1} {X : Type u_5} [TopologicalSpace X] {M : Type u_6} [CommMonoid M] {f : ι → X → M} (hf : LocallyFinite fun i => Function.mulSupport (f i)) (x : X) : ∃ s, ∀ᶠ (y : X) in nhds x, ∏ᶠ (i : ι), f i y = ∏ i ∈ s, f i y
• finsum_eventually_eq_sum 📋 Mathlib.Topology.Algebra.Monoid
  {ι : Type u_1} {X : Type u_5} [TopologicalSpace X] {M : Type u_6} [AddCommMonoid M] {f : ι → X → M} (hf : LocallyFinite fun i => Function.support (f i)) (x : X) : ∃ s, ∀ᶠ (y : X) in nhds x, ∑ᶠ (i : ι), f i y = ∑ i ∈ s, f i y
• ContinuousMap.eventually_mapsTo 📋 Mathlib.Topology.CompactOpen
  {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {K : Set X} {U : Set Y} {f : C(X, Y)} (hK : IsCompact K) (hU : IsOpen U) (h : Set.MapsTo (⇑f) K U) : ∀ᶠ (g : C(X, Y)) in nhds f, Set.MapsTo (⇑g) K U
• ContinuousMap.tendsto_nhds_compactOpen 📋 Mathlib.Topology.CompactOpen
  {α : Type u_1} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace Y] [TopologicalSpace Z] {l : Filter α} {f : α → C(Y, Z)} {g : C(Y, Z)} : Filter.Tendsto f l (nhds g) ↔ ∀ (K : Set Y), IsCompact K → ∀ (U : Set Z), IsOpen U → Set.MapsTo (⇑g) K U → ∀ᶠ (a : α) in l, Set.MapsTo (⇑(f a)) K U
• Filter.tendsto_nhds_atBot_iff 📋 Mathlib.Topology.Filter
  {α : Type u_2} {β : Type u_3} [Preorder β] {l : Filter α} {f : α → Filter β} : Filter.Tendsto f l (nhds Filter.atBot) ↔ ∀ (y : β), ∀ᶠ (a : α) in l, Set.Iic y ∈ f a
• Filter.tendsto_nhds_atTop_iff 📋 Mathlib.Topology.Filter
  {α : Type u_2} {β : Type u_3} [Preorder β] {l : Filter α} {f : α → Filter β} : Filter.Tendsto f l (nhds Filter.atTop) ↔ ∀ (y : β), ∀ᶠ (a : α) in l, Set.Ici y ∈ f a
• Filter.tendsto_nhds 📋 Mathlib.Topology.Filter
  {α : Type u_2} {β : Type u_3} {la : Filter α} {lb : Filter β} {f : α → Filter β} : Filter.Tendsto f la (nhds lb) ↔ ∀ s ∈ lb, ∀ᶠ (a : α) in la, s ∈ f a
• UniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto 📋 Mathlib.Topology.UniformSpace.UniformConvergence
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} (hF : UniformCauchySeqOnFilter F p p') (hF' : ∀ᶠ (x : α) in p', Filter.Tendsto (fun n => F n x) p (nhds (f x))) : TendstoUniformlyOnFilter F f p p'
• TendstoUniformly.tendsto_of_eventually_tendsto 📋 Mathlib.Topology.UniformSpace.UniformConvergence
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} [p.NeBot] {L : ι → β} {ℓ : β} (h1 : TendstoUniformly F f p) (h2 : ∀ᶠ (i : ι) in p, Filter.Tendsto (F i) p' (nhds (L i))) (h3 : Filter.Tendsto L p (nhds ℓ)) : Filter.Tendsto f p' (nhds ℓ)
• TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto 📋 Mathlib.Topology.UniformSpace.UniformConvergence
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} [p.NeBot] {L : ι → β} {ℓ : β} (h1 : TendstoUniformlyOnFilter F f p p') (h2 : ∀ᶠ (i : ι) in p, Filter.Tendsto (F i) p' (nhds (L i))) (h3 : Filter.Tendsto L p (nhds ℓ)) : Filter.Tendsto f p' (nhds ℓ)
• TendstoLocallyUniformly.eq_1 📋 Mathlib.Topology.UniformSpace.LocallyUniformConvergence
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] (F : ι → α → β) (f : α → β) (p : Filter ι) : TendstoLocallyUniformly F f p = ∀ u ∈ uniformity β, ∀ (x : α), ∃ t ∈ nhds x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
• tendsto_comp_of_locally_uniform_limit 📋 Mathlib.Topology.UniformSpace.UniformApproximation
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {x : α} {p : Filter ι} {g : ι → α} (h : ContinuousAt f x) (hg : Filter.Tendsto g p (nhds x)) (hunif : ∀ u ∈ uniformity β, ∃ t ∈ nhds x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u) : Filter.Tendsto (fun n => F n (g n)) p (nhds (f x))
• tendsto_comp_of_locally_uniform_limit_within 📋 Mathlib.Topology.UniformSpace.UniformApproximation
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {x : α} {p : Filter ι} {g : ι → α} (h : ContinuousWithinAt f s x) (hg : Filter.Tendsto g p (nhdsWithin x s)) (hunif : ∀ u ∈ uniformity β, ∃ t ∈ nhdsWithin x s, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u) : Filter.Tendsto (fun n => F n (g n)) p (nhds (f x))
• EquicontinuousAt.eq_1 📋 Mathlib.Topology.UniformSpace.Equicontinuity
  {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] (F : ι → X → α) (x₀ : X) : EquicontinuousAt F x₀ = ∀ U ∈ uniformity α, ∀ᶠ (x : X) in nhds x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U
• Filter.HasBasis.equicontinuousAt_iff_right 📋 Mathlib.Topology.UniformSpace.Equicontinuity
  {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {p : κ → Prop} {s : κ → Set (α × α)} {F : ι → X → α} {x₀ : X} (hα : (uniformity α).HasBasis p s) : EquicontinuousAt F x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in nhds x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k
• IsTopologicalAddGroup.tendstoUniformly_iff 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddGroup G] [u : UniformSpace G] [IsTopologicalAddGroup G] (F : ι → α → G) (f : α → G) (p : Filter ι) (hu : IsTopologicalAddGroup.toUniformSpace G = u) : TendstoUniformly F f p ↔ ∀ u_1 ∈ nhds 0, ∀ᶠ (i : ι) in p, ∀ (a : α), F i a - f a ∈ u_1
• IsTopologicalGroup.tendstoUniformly_iff 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Group G] [u : UniformSpace G] [IsTopologicalGroup G] (F : ι → α → G) (f : α → G) (p : Filter ι) (hu : IsTopologicalGroup.toUniformSpace G = u) : TendstoUniformly F f p ↔ ∀ u_1 ∈ nhds 1, ∀ᶠ (i : ι) in p, ∀ (a : α), F i a / f a ∈ u_1
• IsTopologicalAddGroup.tendstoUniformlyOn_iff 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddGroup G] [u : UniformSpace G] [IsTopologicalAddGroup G] (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α) (hu : IsTopologicalAddGroup.toUniformSpace G = u) : TendstoUniformlyOn F f p s ↔ ∀ u_1 ∈ nhds 0, ∀ᶠ (i : ι) in p, ∀ a ∈ s, F i a - f a ∈ u_1
• IsTopologicalGroup.tendstoUniformlyOn_iff 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Group G] [u : UniformSpace G] [IsTopologicalGroup G] (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α) (hu : IsTopologicalGroup.toUniformSpace G = u) : TendstoUniformlyOn F f p s ↔ ∀ u_1 ∈ nhds 1, ∀ᶠ (i : ι) in p, ∀ a ∈ s, F i a / f a ∈ u_1
• IsTopologicalAddGroup.tendstoLocallyUniformly_iff 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddGroup G] [u : UniformSpace G] [IsTopologicalAddGroup G] [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) (hu : IsTopologicalAddGroup.toUniformSpace G = u) : TendstoLocallyUniformly F f p ↔ ∀ u_1 ∈ nhds 0, ∀ (x : α), ∃ t ∈ nhds x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a - f a ∈ u_1
• IsTopologicalGroup.tendstoLocallyUniformly_iff 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Group G] [u : UniformSpace G] [IsTopologicalGroup G] [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) (hu : IsTopologicalGroup.toUniformSpace G = u) : TendstoLocallyUniformly F f p ↔ ∀ u_1 ∈ nhds 1, ∀ (x : α), ∃ t ∈ nhds x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a / f a ∈ u_1
• IsTopologicalAddGroup.tendstoLocallyUniformlyOn_iff 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddGroup G] [u : UniformSpace G] [IsTopologicalAddGroup G] [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α) (hu : IsTopologicalAddGroup.toUniformSpace G = u) : TendstoLocallyUniformlyOn F f p s ↔ ∀ u_1 ∈ nhds 0, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a - f a ∈ u_1
• IsTopologicalGroup.tendstoLocallyUniformlyOn_iff 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Group G] [u : UniformSpace G] [IsTopologicalGroup G] [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α) (hu : IsTopologicalGroup.toUniformSpace G = u) : TendstoLocallyUniformlyOn F f p s ↔ ∀ u_1 ∈ nhds 1, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a / f a ∈ u_1
• IsLocalMin.inv 📋 Mathlib.Topology.Algebra.Field
  {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Semifield β] [LinearOrder β] [IsStrictOrderedRing β] {f : α → β} {a : α} (h1 : IsLocalMin f a) (h2 : ∀ᶠ (z : α) in nhds a, 0 < f z) : IsLocalMax f⁻¹ a
• Filter.Eventually.exists_gt 📋 Mathlib.Topology.Order.LeftRight
  {α : Type u_1} [TopologicalSpace α] [Preorder α] {a : α} [(nhdsWithin a (Set.Ioi a)).NeBot] {p : α → Prop} (h : ∀ᶠ (x : α) in nhds a, p x) : ∃ b > a, p b
• Filter.Eventually.exists_lt 📋 Mathlib.Topology.Order.LeftRight
  {α : Type u_1} [TopologicalSpace α] [Preorder α] {a : α} [(nhdsWithin a (Set.Iio a)).NeBot] {p : α → Prop} (h : ∀ᶠ (x : α) in nhds a, p x) : ∃ b < a, p b
• 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
• eventually_ge_nhds 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (hab : b < a) : ∀ᶠ (x : α) in nhds a, b ≤ x
• eventually_gt_nhds 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (hab : b < a) : ∀ᶠ (x : α) in nhds a, b < x
• eventually_le_nhds 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (hab : a < b) : ∀ᶠ (x : α) in nhds a, x ≤ b
• eventually_lt_nhds 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {a b : α} (hab : a < b) : ∀ᶠ (x : α) in nhds a, x < b
• eventually_ge_of_tendsto_gt 📋 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
• eventually_gt_of_tendsto_gt 📋 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
• eventually_le_of_tendsto_lt 📋 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
• eventually_lt_of_tendsto_lt 📋 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_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
• ContinuousAt.eventually_lt 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f g : β → α} [TopologicalSpace β] {x₀ : β} (hf : ContinuousAt f x₀) (hg : ContinuousAt g x₀) (hfg : f x₀ < g x₀) : ∀ᶠ (x : β) in nhds x₀, f x < g x
• 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
• ge_mem_nhds 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] {a b : α} (h : a < b) : ∀ᶠ (x : α) in nhds a, x ≤ b
• gt_mem_nhds 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] {a b : α} (h : a < b) : ∀ᶠ (x : α) in nhds a, x < b
• le_mem_nhds 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] {a b : α} (h : a < b) : ∀ᶠ (x : α) in nhds b, a ≤ x
• lt_mem_nhds 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] {a b : α} (h : a < b) : ∀ᶠ (x : α) in nhds b, a < x
• tendsto_order 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [OrderTopology α] {f : β → α} {a : α} {x : Filter β} : Filter.Tendsto f x (nhds a) ↔ (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'
• tendsto_of_tendsto_of_tendsto_of_le_of_le' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [OrderTopology α] {f g h : β → α} {b : Filter β} {a : α} (hg : Filter.Tendsto g b (nhds a)) (hh : Filter.Tendsto h b (nhds a)) (hgf : ∀ᶠ (b : β) in b, g b ≤ f b) (hfh : ∀ᶠ (b : β) in b, f b ≤ h b) : Filter.Tendsto f b (nhds a)
• Filter.Tendsto.squeeze' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [OrderTopology α] {f g h : β → α} {b : Filter β} {a : α} (hg : Filter.Tendsto g b (nhds a)) (hh : Filter.Tendsto h b (nhds a)) (hgf : ∀ᶠ (b : β) in b, g b ≤ f b) (hfh : ∀ᶠ (b : β) in b, f b ≤ h b) : Filter.Tendsto f b (nhds a)
• tendsto_order_unbounded 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [OrderTopology α] {f : β → α} {a : α} {x : Filter β} (hu : ∃ u, a < u) (hl : ∃ l, l < a) (h : ∀ (l u : α), l < a → a < u → ∀ᶠ (b : β) in x, l < f b ∧ f b < u) : Filter.Tendsto f x (nhds a)
• Filter.Eventually.exists_Ioo_subset 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] {a : α} {p : α → Prop} (hp : ∀ᶠ (x : α) in nhds a, p x) : ∃ l u, a ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ {x | p x}
• eventually_abs_sub_lt 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [OrderTopology α] (a : α) {ε : α} (hε : 0 < ε) : ∀ᶠ (x : α) in nhds a, |x - a| < ε
• eventually_mabs_div_lt 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] (a : α) {ε : α} (hε : 1 < ε) : ∀ᶠ (x : α) in nhds a, mabs (x / a) < ε
• LinearOrderedAddCommGroup.tendsto_nhds 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [OrderTopology α] {f : β → α} {x : Filter β} {a : α} : Filter.Tendsto f x (nhds a) ↔ ∀ ε > 0, ∀ᶠ (b : β) in x, |f b - a| < ε
• LinearOrderedCommGroup.tendsto_nhds 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] {f : β → α} {x : Filter β} {a : α} : Filter.Tendsto f x (nhds a) ↔ ∀ ε > 1, ∀ᶠ (b : β) in x, mabs (f b / a) < ε
• tendsto_bdd_div_atTop_nhds_zero 📋 Mathlib.Topology.Algebra.Order.Field
  {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {b B : 𝕜} (hb : ∀ᶠ (x : α) in l, b ≤ f x) (hB : ∀ᶠ (x : α) in l, f x ≤ B) (hg : Filter.Tendsto g l Filter.atTop) : Filter.Tendsto (fun x => f x / g x) l (nhds 0)
• bdd_le_mul_tendsto_zero' 📋 Mathlib.Topology.Algebra.Order.Field
  {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} (C : 𝕜) (hf : ∀ᶠ (x : α) in l, |f x| ≤ C) (hg : Filter.Tendsto g l (nhds 0)) : Filter.Tendsto (fun x => f x * g x) l (nhds 0)
• bdd_le_mul_tendsto_zero 📋 Mathlib.Topology.Algebra.Order.Field
  {𝕜 : Type u_1} {α : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {b B : 𝕜} (hb : ∀ᶠ (x : α) in l, b ≤ f x) (hB : ∀ᶠ (x : α) in l, f x ≤ B) (hg : Filter.Tendsto g l (nhds 0)) : Filter.Tendsto (fun x => f x * g x) l (nhds 0)
• PartialHomeomorph.eventually_left_inverse 📋 Mathlib.Topology.PartialHomeomorph
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : ∀ᶠ (y : X) in nhds x, ↑e.symm (↑e y) = y
• PartialHomeomorph.eventually_right_inverse 📋 Mathlib.Topology.PartialHomeomorph
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {x : Y} (hx : x ∈ e.target) : ∀ᶠ (y : Y) in nhds x, ↑e (↑e.symm y) = y
• PartialHomeomorph.eventually_nhds 📋 Mathlib.Topology.PartialHomeomorph
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {x : X} (p : Y → Prop) (hx : x ∈ e.source) : (∀ᶠ (y : Y) in nhds (↑e x), p y) ↔ ∀ᶠ (x : X) in nhds x, p (↑e x)
• PartialHomeomorph.eventually_right_inverse' 📋 Mathlib.Topology.PartialHomeomorph
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : ∀ᶠ (y : Y) in nhds (↑e x), ↑e (↑e.symm y) = y
• PartialHomeomorph.eventually_nhds' 📋 Mathlib.Topology.PartialHomeomorph
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {x : X} (p : X → Prop) (hx : x ∈ e.source) : (∀ᶠ (y : Y) in nhds (↑e x), p (↑e.symm y)) ↔ ∀ᶠ (x : X) in nhds x, p x
• PartialHomeomorph.eventually_left_inverse' 📋 Mathlib.Topology.PartialHomeomorph
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {x : Y} (hx : x ∈ e.target) : ∀ᶠ (y : X) in nhds (↑e.symm x), ↑e.symm (↑e y) = y
• EMetric.tendsto_nhds 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] {f : Filter β} {u : β → α} {a : α} : Filter.Tendsto u f (nhds a) ↔ ∀ ε > 0, ∀ᶠ (x : β) in f, edist (u x) a < ε
• EMetric.tendstoLocallyUniformly_iff 📋 Mathlib.Topology.EMetricSpace.Basic
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] {ι : Type u_2} [TopologicalSpace β] {F : ι → β → α} {f : β → α} {p : Filter ι} : TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ (x : β), ∃ t ∈ nhds x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
• Metric.eventually_nhds_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {p : α → Prop} : (∀ᶠ (y : α) in nhds x, p y) ↔ ∃ ε > 0, ∀ ⦃y : α⦄, dist y x < ε → p y
• Metric.eventually_nhds_iff_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {p : α → Prop} : (∀ᶠ (y : α) in nhds x, p y) ↔ ∃ ε > 0, ∀ y ∈ Metric.ball x ε, p y
• Metric.tendsto_nhds 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : Filter β} {u : β → α} {a : α} : Filter.Tendsto u f (nhds a) ↔ ∀ ε > 0, ∀ᶠ (x : β) in f, dist (u x) a < ε
• Metric.continuous_iff' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : β → α} : Continuous f ↔ ∀ (a : β), ∀ ε > 0, ∀ᶠ (x : β) in nhds a, dist (f x) (f a) < ε
• Metric.continuousAt_iff' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : β → α} {b : β} : ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in nhds b, dist (f x) (f b) < ε
• Metric.eventually_nhds_prod_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f : Filter ι} {x₀ : α} {p : α × ι → Prop} : (∀ᶠ (x : α × ι) in nhds x₀ ×ˢ f, p x) ↔ ∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i)
• Metric.eventually_prod_nhds_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f : Filter ι} {x₀ : α} {p : ι × α → Prop} : (∀ᶠ (x : ι × α) in f ×ˢ nhds x₀, p x) ↔ ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)
• Metric.tendstoLocallyUniformly_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Basic
  {α : Type u} {β : Type v} {ι : Type u_1} [PseudoMetricSpace α] [TopologicalSpace β] {F : ι → β → α} {f : β → α} {p : Filter ι} : TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ (x : β), ∃ t ∈ nhds x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε
• Metric.eventually_isCompact_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] [WeaklyLocallyCompactSpace α] (x : α) : ∀ᶠ (r : ℝ) in nhds 0, IsCompact (Metric.closedBall x r)
• eventually_closedBall_subset 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] {x : α} {u : Set α} (hu : u ∈ nhds x) : ∀ᶠ (r : ℝ) in nhds 0, Metric.closedBall x r ⊆ u
• squeeze_zero' 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_3} {f g : α → ℝ} {t₀ : Filter α} (hf : ∀ᶠ (t : α) in t₀, 0 ≤ f t) (hft : ∀ᶠ (t : α) in t₀, f t ≤ g t) (g0 : Filter.Tendsto g t₀ (nhds 0)) : Filter.Tendsto f t₀ (nhds 0)
• ENNReal.tendsto_nhds_top_iff_nnreal 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {α : Type u_1} {m : α → ENNReal} {f : Filter α} : Filter.Tendsto m f (nhds ⊤) ↔ ∀ (x : NNReal), ∀ᶠ (a : α) in f, ↑x < m a
• ENNReal.tendsto_nhds_top 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {α : Type u_1} {m : α → ENNReal} {f : Filter α} (h : ∀ (n : ℕ), ∀ᶠ (a : α) in f, ↑n < m a) : Filter.Tendsto m f (nhds ⊤)
• ENNReal.tendsto_nhds_top_iff_nat 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {α : Type u_1} {m : α → ENNReal} {f : Filter α} : Filter.Tendsto m f (nhds ⊤) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in f, ↑n < m a
• ENNReal.tendsto_nhds_zero 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {α : Type u_1} {f : Filter α} {u : α → ENNReal} : Filter.Tendsto u f (nhds 0) ↔ ∀ ε > 0, ∀ᶠ (x : α) in f, u x ≤ ε
• ENNReal.tendsto_nhds_of_Icc 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal} (h : ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Set.Icc (a - ε) (a + ε)) : Filter.Tendsto u f (nhds a)
• ENNReal.tendsto_nhds 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal} (ha : a ≠ ⊤) : Filter.Tendsto u f (nhds a) ↔ ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Set.Icc (a - ε) (a + ε)
• LowerSemicontinuousAt.eq_1 📋 Mathlib.Topology.Semicontinuous
  {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : α → β) (x : α) : LowerSemicontinuousAt f x = ∀ y < f x, ∀ᶠ (x' : α) in nhds x, y < f x'
• UpperSemicontinuousAt.eq_1 📋 Mathlib.Topology.Semicontinuous
  {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] (f : α → β) (x : α) : UpperSemicontinuousAt f x = ∀ (y : β), f x < y → ∀ᶠ (x' : α) in nhds x, f x' < y
• lowerSemicontinuousAt_ciSup 📋 Mathlib.Topology.Semicontinuous
  {α : Type u_1} [TopologicalSpace α] {x : α} {ι : Sort u_3} {δ' : Type u_5} [ConditionallyCompleteLinearOrder δ'] {f : ι → α → δ'} (bdd : ∀ᶠ (y : α) in nhds x, BddAbove (Set.range fun i => f i y)) (h : ∀ (i : ι), LowerSemicontinuousAt (f i) x) : LowerSemicontinuousAt (fun x' => ⨆ i, f i x') x
• upperSemicontinuousAt_ciInf 📋 Mathlib.Topology.Semicontinuous
  {α : Type u_1} [TopologicalSpace α] {x : α} {ι : Sort u_3} {δ' : Type u_5} [ConditionallyCompleteLinearOrder δ'] {f : ι → α → δ'} (bdd : ∀ᶠ (y : α) in nhds x, BddBelow (Set.range fun i => f i y)) (h : ∀ (i : ι), UpperSemicontinuousAt (f i) x) : UpperSemicontinuousAt (fun x' => ⨅ i, f i x') x
• EReal.tendsto_nhds_bot_iff_real 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_2} {m : α → EReal} {f : Filter α} : Filter.Tendsto m f (nhds ⊥) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, m a < ↑x
• EReal.tendsto_nhds_top_iff_real 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_2} {m : α → EReal} {f : Filter α} : Filter.Tendsto m f (nhds ⊤) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, ↑x < m a
• ENNReal.aemeasurable_of_tendsto 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Real
  {α : Type u_1} {mα : MeasurableSpace α} {f : ℕ → α → ENNReal} {g : α → ENNReal} {μ : MeasureTheory.Measure α} (hf : ∀ (i : ℕ), AEMeasurable (f i) μ) (hlim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun i => f i a) Filter.atTop (nhds (g a))) : AEMeasurable g μ
• ENNReal.aemeasurable_of_tendsto' 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Real
  {α : Type u_1} {mα : MeasurableSpace α} {ι : Type u_5} {f : ι → α → ENNReal} {g : α → ENNReal} {μ : MeasureTheory.Measure α} (u : Filter ι) [u.NeBot] [u.IsCountablyGenerated] (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hlim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun i => f i a) u (nhds (g a))) : AEMeasurable g μ
• MeasureTheory.lintegral_tendsto_of_tendsto_of_monotone 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Add
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} {F : α → ENNReal} (hf : ∀ (n : ℕ), AEMeasurable (f n) μ) (h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x) (h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (F x))) : Filter.Tendsto (fun n => ∫⁻ (x : α), f n x ∂μ) Filter.atTop (nhds (∫⁻ (x : α), F x ∂μ))
• NormedAddCommGroup.tendsto_nhds_zero 📋 Mathlib.Analysis.Normed.Group.Basic
  {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] {f : α → E} {l : Filter α} : Filter.Tendsto f l (nhds 0) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
• NormedCommGroup.tendsto_nhds_one 📋 Mathlib.Analysis.Normed.Group.Basic
  {α : Type u_2} {E : Type u_5} [SeminormedGroup E] {f : α → E} {l : Filter α} : Filter.Tendsto f l (nhds 1) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
• SeminormedAddGroup.disjoint_nhds 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_5} [SeminormedAddGroup E] (x : E) (f : Filter E) : Disjoint (nhds x) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y - x‖
• SeminormedAddGroup.disjoint_nhds_zero 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_5} [SeminormedAddGroup E] (f : Filter E) : Disjoint (nhds 0) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y‖
• SeminormedGroup.disjoint_nhds 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_5} [SeminormedGroup E] (x : E) (f : Filter E) : Disjoint (nhds x) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y / x‖
• SeminormedGroup.disjoint_nhds_one 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_5} [SeminormedGroup E] (f : Filter E) : Disjoint (nhds 1) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y‖
• squeeze_one_norm' 📋 Mathlib.Analysis.Normed.Group.Continuity
  {α : Type u_2} {E : Type u_5} [SeminormedGroup E] {f : α → E} {a : α → ℝ} {t₀ : Filter α} (h : ∀ᶠ (n : α) in t₀, ‖f n‖ ≤ a n) (h' : Filter.Tendsto a t₀ (nhds 0)) : Filter.Tendsto f t₀ (nhds 1)
• squeeze_zero_norm' 📋 Mathlib.Analysis.Normed.Group.Continuity
  {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] {f : α → E} {a : α → ℝ} {t₀ : Filter α} (h : ∀ᶠ (n : α) in t₀, ‖f n‖ ≤ a n) (h' : Filter.Tendsto a t₀ (nhds 0)) : Filter.Tendsto f t₀ (nhds 0)
• eventually_nhds_norm_smul_sub_lt 📋 Mathlib.Analysis.Normed.Module.Basic
  {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (c : 𝕜) (x : E) {ε : ℝ} (h : 0 < ε) : ∀ᶠ (y : E) in nhds x, ‖c • (y - x)‖ < ε
• Metric.eventually_notMem_cthickening_of_infEdist_pos 📋 Mathlib.Topology.MetricSpace.Thickening
  {α : Type u} [PseudoEMetricSpace α] {E : Set α} {x : α} (h : x ∉ closure E) : ∀ᶠ (δ : ℝ) in nhds 0, x ∉ Metric.cthickening δ E
• Metric.eventually_notMem_thickening_of_infEdist_pos 📋 Mathlib.Topology.MetricSpace.Thickening
  {α : Type u} [PseudoEMetricSpace α] {E : Set α} {x : α} (h : x ∉ closure E) : ∀ᶠ (δ : ℝ) in nhds 0, x ∉ Metric.thickening δ E
• Metric.eventually_not_mem_cthickening_of_infEdist_pos 📋 Mathlib.Topology.MetricSpace.Thickening
  {α : Type u} [PseudoEMetricSpace α] {E : Set α} {x : α} (h : x ∉ closure E) : ∀ᶠ (δ : ℝ) in nhds 0, x ∉ Metric.cthickening δ E
• Metric.eventually_not_mem_thickening_of_infEdist_pos 📋 Mathlib.Topology.MetricSpace.Thickening
  {α : Type u} [PseudoEMetricSpace α] {E : Set α} {x : α} (h : x ∉ closure E) : ∀ᶠ (δ : ℝ) in nhds 0, x ∉ Metric.thickening δ E
• tendsto_indicator_const_apply_iff_eventually 📋 Mathlib.Topology.IndicatorConstPointwise
  {α : Type u_1} {A : Set α} {β : Type u_2} [Zero β] [TopologicalSpace β] {ι : Type u_3} (L : Filter ι) {As : ι → Set α} [T1Space β] (b : β) [NeZero b] (x : α) : Filter.Tendsto (fun i => (As i).indicator (fun x => b) x) L (nhds (A.indicator (fun x => b) x)) ↔ ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
• tendsto_indicator_const_iff_forall_eventually 📋 Mathlib.Topology.IndicatorConstPointwise
  {α : Type u_1} {A : Set α} {β : Type u_2} [Zero β] [TopologicalSpace β] {ι : Type u_3} (L : Filter ι) {As : ι → Set α} [T1Space β] (b : β) [NeZero b] : Filter.Tendsto (fun i => (As i).indicator fun x => b) L (nhds (A.indicator fun x => b)) ↔ ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
• tendsto_indicator_const_apply_iff_eventually' 📋 Mathlib.Topology.IndicatorConstPointwise
  {α : Type u_1} {A : Set α} {β : Type u_2} [Zero β] [TopologicalSpace β] {ι : Type u_3} (L : Filter ι) {As : ι → Set α} (b : β) (nhds_b : {0}ᶜ ∈ nhds b) (nhds_o : {b}ᶜ ∈ nhds 0) (x : α) : Filter.Tendsto (fun i => (As i).indicator (fun x => b) x) L (nhds (A.indicator (fun x => b) x)) ↔ ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
• tendsto_indicator_const_iff_forall_eventually' 📋 Mathlib.Topology.IndicatorConstPointwise
  {α : Type u_1} {A : Set α} {β : Type u_2} [Zero β] [TopologicalSpace β] {ι : Type u_3} (L : Filter ι) {As : ι → Set α} (b : β) (nhds_b : {0}ᶜ ∈ nhds b) (nhds_o : {b}ᶜ ∈ nhds 0) : Filter.Tendsto (fun i => (As i).indicator fun x => b) L (nhds (A.indicator fun x => b)) ↔ ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
• aemeasurable_of_tendsto_metrizable_ae' 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] {μ : MeasureTheory.Measure α} {f : ℕ → α → β} {g : α → β} (hf : ∀ (n : ℕ), AEMeasurable (f n) μ) (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) : AEMeasurable g μ
• measurable_of_tendsto_metrizable_ae 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] {μ : MeasureTheory.Measure α} [μ.IsComplete] {f : ℕ → α → β} {g : α → β} (hf : ∀ (n : ℕ), Measurable (f n)) (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) : Measurable g
• aemeasurable_of_tendsto_metrizable_ae 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] {ι : Type u_3} {μ : MeasureTheory.Measure α} {f : ι → α → β} {g : α → β} (u : Filter ι) [hu : u.NeBot] [u.IsCountablyGenerated] (hf : ∀ (n : ι), AEMeasurable (f n) μ) (h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) u (nhds (g x))) : AEMeasurable g μ
• measurable_limit_of_tendsto_metrizable_ae 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] {ι : Type u_3} [Countable ι] [Nonempty ι] {μ : MeasureTheory.Measure α} {f : ι → α → β} {L : Filter ι} [L.IsCountablyGenerated] (hf : ∀ (n : ι), AEMeasurable (f n) μ) (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Filter.Tendsto (fun n => f n x) L (nhds l)) : ∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) L (nhds (f_lim x))
• MeasureTheory.StronglyMeasurable.tendsto_approxBounded_ae 📋 Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
  {α : Type u_1} {β : Type u_5} {f : α → β} [NormedAddCommGroup β] [NormedSpace ℝ β] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hf : MeasureTheory.StronglyMeasurable f) {c : ℝ} (hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c) : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => (hf.approxBounded c n) x) Filter.atTop (nhds (f x))
• aestronglyMeasurable_of_tendsto_ae 📋 Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
  {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_5} [TopologicalSpace.PseudoMetrizableSpace β] (u : Filter ι) [u.NeBot] [u.IsCountablyGenerated] {f : ι → α → β} {g : α → β} (hf : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) (lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) u (nhds (g x))) : MeasureTheory.AEStronglyMeasurable g μ
• exists_stronglyMeasurable_limit_of_tendsto_ae 📋 Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
  {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace.PseudoMetrizableSpace β] {f : ℕ → α → β} (hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds l)) : ∃ f_lim, MeasureTheory.StronglyMeasurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (f_lim x))
• MeasureTheory.lintegral_tendsto_of_tendsto_of_antitone 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Sub
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} {F : α → ENNReal} (hf : ∀ (n : ℕ), AEMeasurable (f n) μ) (h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n => f n x) (h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤) (h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (F x))) : Filter.Tendsto (fun n => ∫⁻ (x : α), f n x ∂μ) Filter.atTop (nhds (∫⁻ (x : α), F x ∂μ))
• MeasureTheory.tendsto_lintegral_of_dominated_convergence 📋 Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : ℕ → α → ENNReal} {f : α → ENNReal} (bound : α → ENNReal) (hF_meas : ∀ (n : ℕ), Measurable (F n)) (h_bound : ∀ (n : ℕ), F n ≤ᵐ[μ] bound) (h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) : Filter.Tendsto (fun n => ∫⁻ (a : α), F n a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), f a ∂μ))
• MeasureTheory.tendsto_lintegral_of_dominated_convergence' 📋 Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : ℕ → α → ENNReal} {f : α → ENNReal} (bound : α → ENNReal) (hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ) (h_bound : ∀ (n : ℕ), F n ≤ᵐ[μ] bound) (h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) : Filter.Tendsto (fun n => ∫⁻ (a : α), F n a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), f a ∂μ))
• MeasureTheory.tendsto_lintegral_filter_of_dominated_convergence 📋 Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : Type u_2} {l : Filter ι} [l.IsCountablyGenerated] {F : ι → α → ENNReal} {f : α → ENNReal} (bound : α → ENNReal) (hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)) (h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) (h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) l (nhds (f a))) : Filter.Tendsto (fun n => ∫⁻ (a : α), F n a ∂μ) l (nhds (∫⁻ (a : α), f a ∂μ))
• MeasureTheory.tendsto_of_lintegral_tendsto_of_monotone 📋 Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
  {α : Type u_2} {mα : MeasurableSpace α} {f : ℕ → α → ENNReal} {F : α → ENNReal} {μ : MeasureTheory.Measure α} (hF_meas : AEMeasurable F μ) (hf_tendsto : Filter.Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), F a ∂μ))) (hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a) (h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a) (h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤) : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun i => f i a) Filter.atTop (nhds (F a))
• MeasureTheory.tendsto_of_lintegral_tendsto_of_antitone 📋 Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
  {α : Type u_2} {mα : MeasurableSpace α} {f : ℕ → α → ENNReal} {F : α → ENNReal} {μ : MeasureTheory.Measure α} (hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ) (hf_tendsto : Filter.Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), F a ∂μ))) (hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a) (h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a) (h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤) : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun i => f i a) Filter.atTop (nhds (F a))
• MeasureTheory.tendsto_of_lintegral_tendsto_of_monotone_aux 📋 Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
  {α : Type u_2} {mα : MeasurableSpace α} {f : ℕ → α → ENNReal} {F : α → ENNReal} {μ : MeasureTheory.Measure α} (hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ) (hF_meas : AEMeasurable F μ) (hf_tendsto : Filter.Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), F a ∂μ))) (hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a) (h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a) (h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤) : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun i => f i a) Filter.atTop (nhds (F a))
• MeasureTheory.eventually_nhds_one_measure_smul_diff_lt 📋 Mathlib.MeasureTheory.Group.Measure
  {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] {k : Set G} (hk : IsCompact k) (h'k : IsClosed k) {ε : ENNReal} (hε : ε ≠ 0) : ∀ᶠ (g : G) in nhds 1, μ (g • k \ k) < ε
• MeasureTheory.eventually_nhds_zero_measure_vadd_diff_lt 📋 Mathlib.MeasureTheory.Group.Measure
  {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] {k : Set G} (hk : IsCompact k) (h'k : IsClosed k) {ε : ENNReal} (hε : ε ≠ 0) : ∀ᶠ (g : G) in nhds 0, μ ((g +ᵥ k) \ k) < ε
• MeasureTheory.all_ae_tendsto_ofReal_norm 📋 Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
  {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {F : ℕ → α → β} {f : α → β} (h : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => ENNReal.ofReal ‖F n a‖) Filter.atTop (nhds (ENNReal.ofReal ‖f a‖))
• MeasureTheory.ae_tendsto_enorm 📋 Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [TopologicalSpace ε] [ENormedAddMonoid ε] {F' : ℕ → α → ε} {f' : α → ε} (h : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F' n a) Filter.atTop (nhds (f' a))) : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => ‖F' n a‖ₑ) Filter.atTop (nhds ‖f' a‖ₑ)
• MeasureTheory.hasFiniteIntegral_of_dominated_convergence_enorm 📋 Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [TopologicalSpace ε] [ENormedAddMonoid ε] {F' : ℕ → α → ε} {f' : α → ε} {bound' : α → ENNReal} (bound_hasFiniteIntegral : MeasureTheory.HasFiniteIntegral bound' μ) (h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F' n a‖ₑ ≤ bound' a) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F' n a) Filter.atTop (nhds (f' a))) : MeasureTheory.HasFiniteIntegral f' μ
• MeasureTheory.all_ae_ofReal_f_le_bound 📋 Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
  {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {F : ℕ → α → β} {f : α → β} {bound : α → ℝ} (h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) : ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
• MeasureTheory.ae_enorm_le_bound 📋 Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [TopologicalSpace ε] [ENormedAddMonoid ε] {F' : ℕ → α → ε} {f' : α → ε} {bound' : α → ENNReal} (h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F' n a‖ₑ ≤ bound' a) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F' n a) Filter.atTop (nhds (f' a))) : ∀ᵐ (a : α) ∂μ, ‖f' a‖ₑ ≤ bound' a
• MeasureTheory.hasFiniteIntegral_of_dominated_convergence 📋 Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
  {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {F : ℕ → α → β} {f : α → β} {bound : α → ℝ} (bound_hasFiniteIntegral : MeasureTheory.HasFiniteIntegral bound μ) (h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) : MeasureTheory.HasFiniteIntegral f μ
• MeasureTheory.tendsto_lintegral_norm_of_dominated_convergence 📋 Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
  {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {F : ℕ → α → β} {f : α → β} {bound : α → ℝ} (F_measurable : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) μ) (bound_hasFiniteIntegral : MeasureTheory.HasFiniteIntegral bound μ) (h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) : Filter.Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) Filter.atTop (nhds 0)
• MeasureTheory.Egorov.measure_inter_notConvergentSeq_eq_zero 📋 Mathlib.MeasureTheory.Function.Egorov
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [PseudoEMetricSpace β] {μ : MeasureTheory.Measure α} {s : Set α} {f : ι → α → β} {g : α → β} [SemilatticeSup ι] [Nonempty ι] (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) (n : ℕ) : μ (s ∩ ⋂ j, MeasureTheory.Egorov.notConvergentSeq f g n j) = 0
• MeasureTheory.Egorov.iUnionNotConvergentSeq 📋 Mathlib.MeasureTheory.Function.Egorov
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [PseudoEMetricSpace β] {μ : MeasureTheory.Measure α} {s : Set α} {ε : ℝ} {f : ι → α → β} {g : α → β} [SemilatticeSup ι] [Nonempty ι] [Countable ι] (hε : 0 < ε) (hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)) (hg : MeasureTheory.StronglyMeasurable g) (hsm : MeasurableSet s) (hs : μ s ≠ ⊤) (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) : Set α
• MeasureTheory.Egorov.notConvergentSeqLTIndex 📋 Mathlib.MeasureTheory.Function.Egorov
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [PseudoEMetricSpace β] {μ : MeasureTheory.Measure α} {s : Set α} {ε : ℝ} {f : ι → α → β} {g : α → β} [SemilatticeSup ι] [Nonempty ι] [Countable ι] (hε : 0 < ε) (hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)) (hg : MeasureTheory.StronglyMeasurable g) (hsm : MeasurableSet s) (hs : μ s ≠ ⊤) (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) (n : ℕ) : ι
• MeasureTheory.Egorov.iUnionNotConvergentSeq_measurableSet 📋 Mathlib.MeasureTheory.Function.Egorov
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [PseudoEMetricSpace β] {μ : MeasureTheory.Measure α} {s : Set α} {ε : ℝ} {f : ι → α → β} {g : α → β} [SemilatticeSup ι] [Nonempty ι] [Countable ι] (hε : 0 < ε) (hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)) (hg : MeasureTheory.StronglyMeasurable g) (hsm : MeasurableSet s) (hs : μ s ≠ ⊤) (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) : MeasurableSet (MeasureTheory.Egorov.iUnionNotConvergentSeq hε hf hg hsm hs hfg)
• MeasureTheory.Egorov.iUnionNotConvergentSeq_subset 📋 Mathlib.MeasureTheory.Function.Egorov
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [PseudoEMetricSpace β] {μ : MeasureTheory.Measure α} {s : Set α} {ε : ℝ} {f : ι → α → β} {g : α → β} [SemilatticeSup ι] [Nonempty ι] [Countable ι] (hε : 0 < ε) (hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)) (hg : MeasureTheory.StronglyMeasurable g) (hsm : MeasurableSet s) (hs : μ s ≠ ⊤) (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) : MeasureTheory.Egorov.iUnionNotConvergentSeq hε hf hg hsm hs hfg ⊆ s
• MeasureTheory.tendstoUniformlyOn_of_ae_tendsto' 📋 Mathlib.MeasureTheory.Function.Egorov
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [PseudoEMetricSpace β] {μ : MeasureTheory.Measure α} [SemilatticeSup ι] [Nonempty ι] [Countable ι] {f : ι → α → β} {g : α → β} [MeasureTheory.IsFiniteMeasure μ] (hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)) (hg : MeasureTheory.StronglyMeasurable g) (hfg : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) {ε : ℝ} (hε : 0 < ε) : ∃ t, MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g Filter.atTop tᶜ
• MeasureTheory.Egorov.measure_notConvergentSeq_tendsto_zero 📋 Mathlib.MeasureTheory.Function.Egorov
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [PseudoEMetricSpace β] {μ : MeasureTheory.Measure α} {s : Set α} {f : ι → α → β} {g : α → β} [SemilatticeSup ι] [Countable ι] (hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)) (hg : MeasureTheory.StronglyMeasurable g) (hsm : MeasurableSet s) (hs : μ s ≠ ⊤) (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) (n : ℕ) : Filter.Tendsto (fun j => μ (s ∩ MeasureTheory.Egorov.notConvergentSeq f g n j)) Filter.atTop (nhds 0)

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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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 ?a

   If 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 ?b

4. By 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 find tsum_lt_tsum even though the hypothesis f i < g i is 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 2c2d6a2 serving mathlib revision a2882c0