Loogle!

Result

Found 347 declarations whose name contains "onFun". Of these, only the first 200 are shown.

• Lean.ProjectionFunctionInfo 📋 Lean.ProjFns
  : Type
• Lean.instInhabitedProjectionFunctionInfo.default 📋 Lean.ProjFns
  : Lean.ProjectionFunctionInfo
• Lean.instInhabitedProjectionFunctionInfo 📋 Lean.ProjFns
  : Inhabited Lean.ProjectionFunctionInfo
• Lean.instReprProjectionFunctionInfo 📋 Lean.ProjFns
  : Repr Lean.ProjectionFunctionInfo
• Lean.ProjectionFunctionInfo.ctorName 📋 Lean.ProjFns
  (self : Lean.ProjectionFunctionInfo) : Lean.Name
• Lean.ProjectionFunctionInfo.fromClass 📋 Lean.ProjFns
  (self : Lean.ProjectionFunctionInfo) : Bool
• Lean.ProjectionFunctionInfo.fromClassEx 📋 Lean.ProjFns
  (info : Lean.ProjectionFunctionInfo) : Bool
• Lean.ProjectionFunctionInfo.i 📋 Lean.ProjFns
  (self : Lean.ProjectionFunctionInfo) : ℕ
• Lean.ProjectionFunctionInfo.numParams 📋 Lean.ProjFns
  (self : Lean.ProjectionFunctionInfo) : ℕ
• Lean.instReprProjectionFunctionInfo.repr 📋 Lean.ProjFns
  : Lean.ProjectionFunctionInfo → ℕ → Std.Format
• Lean.ProjectionFunctionInfo.mk 📋 Lean.ProjFns
  (ctorName : Lean.Name) (numParams i : ℕ) (fromClass : Bool) : Lean.ProjectionFunctionInfo
• Lean.ProjectionFunctionInfo.mk.injEq 📋 Lean.ProjFns
  (ctorName : Lean.Name) (numParams i : ℕ) (fromClass : Bool) (ctorName✝ : Lean.Name) (numParams✝ i✝ : ℕ) (fromClass✝ : Bool) : ({ ctorName := ctorName, numParams := numParams, i := i, fromClass := fromClass } = { ctorName := ctorName✝, numParams := numParams✝, i := i✝, fromClass := fromClass✝ }) = (ctorName = ctorName✝ ∧ numParams = numParams✝ ∧ i = i✝ ∧ fromClass = fromClass✝)
• Lean.ProjectionFunctionInfo.mk.sizeOf_spec 📋 Lean.ProjFns
  (ctorName : Lean.Name) (numParams i : ℕ) (fromClass : Bool) : sizeOf { ctorName := ctorName, numParams := numParams, i := i, fromClass := fromClass } = 1 + sizeOf ctorName + sizeOf numParams + sizeOf i + sizeOf fromClass
• Lean.mkModuleInitializationFunctionName 📋 Lean.Compiler.NameMangling
  (moduleName : Lean.Name) : String
• Lean.Meta.mkFixOfMonFun 📋 Lean.Meta.Order
  (packedType packedInst hmono : Lean.Expr) : Lean.MetaM Lean.Expr
• Lean.Firefox.instFromJsonFuncTable 📋 Lean.Util.Profiler
  : Lean.FromJson Lean.Firefox.FuncTable
• Lean.Firefox.instToJsonFuncTable 📋 Lean.Util.Profiler
  : Lean.ToJson Lean.Firefox.FuncTable
• Lean.Firefox.instToJsonFuncTable.toJson 📋 Lean.Util.Profiler
  : Lean.Firefox.FuncTable → Lean.Json
• Lean.Firefox.instFromJsonFuncTable.fromJson 📋 Lean.Util.Profiler
  : Lean.Json → Except String Lean.Firefox.FuncTable
• Function.onFun 📋 Mathlib.Logic.Function.Defs
  {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} (f : β → β → φ) (g : α → β) : α → α → φ
• Function.onFun_apply 📋 Mathlib.Logic.Function.Basic
  {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : β → β → γ) (g : α → β) (a b : α) : Function.onFun f g a b = f (g a) (g b)
• directedOn_onFun_iff 📋 Mathlib.Order.Directed
  {α : Type u} {β : Type v} {r : α → α → Prop} {f : β → α} {s : Set β} : DirectedOn (Function.onFun r f) s ↔ DirectedOn r (f '' s)
• WellFounded.onFun 📋 Mathlib.Order.WellFounded
  {α : Sort u_4} {β : Sort u_5} {r : β → β → Prop} {f : α → β} : WellFounded r → WellFounded (Function.onFun r f)
• Function.onFun.eq_1 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} (f : β → β → φ) (g : α → β) (x y : α) : Function.onFun f g x y = f (g x) (g y)
• CategoryTheory.toSkeletonFunctor 📋 Mathlib.CategoryTheory.Skeletal
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Functor C (CategoryTheory.Skeleton C)
• CategoryTheory.toSkeletonFunctor_obj 📋 Mathlib.CategoryTheory.Skeletal
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.toSkeletonFunctor C).obj X = CategoryTheory.toSkeleton X
• CategoryTheory.Functor.toSkeletonFunctorCompMapSkeletonIso 📋 Mathlib.CategoryTheory.Skeletal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : (CategoryTheory.toSkeletonFunctor C).comp F.mapSkeleton ≅ F.comp (CategoryTheory.toSkeletonFunctor D)
• CategoryTheory.toSkeletonFunctor_map 📋 Mathlib.CategoryTheory.Skeletal
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.toSkeletonFunctor C).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.preCounitIso X).hom (CategoryTheory.CategoryStruct.comp f (CategoryTheory.preCounitIso Y).inv)
• CategoryTheory.MorphismProperty.instHasFunctorialFactorizationFunctorFunctorCategory 📋 Mathlib.CategoryTheory.MorphismProperty.Factorization
  {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) [W₁.HasFunctorialFactorization W₂] (J : Type u_2) [CategoryTheory.Category.{u_4, u_2} J] : (W₁.functorCategory J).HasFunctorialFactorization (W₂.functorCategory J)
• CategoryTheory.Functor.mapMonFunctor 📋 Mathlib.CategoryTheory.Monoidal.Mon_
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] : CategoryTheory.Functor (CategoryTheory.LaxMonoidalFunctor C D) (CategoryTheory.Functor (Mon C) (Mon D))
• CategoryTheory.Functor.mapMonFunctor_obj 📋 Mathlib.CategoryTheory.Monoidal.Mon_
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.LaxMonoidalFunctor C D) : (CategoryTheory.Functor.mapMonFunctor C D).obj F = F.mapMon
• CategoryTheory.Functor.mapMonFunctor_map_app_hom 📋 Mathlib.CategoryTheory.Monoidal.Mon_
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {X✝ Y✝ : CategoryTheory.LaxMonoidalFunctor C D} (α : X✝ ⟶ Y✝) (A : Mon C) : (((CategoryTheory.Functor.mapMonFunctor C D).map α).app A).hom = α.hom.app A.X
• CategoryTheory.Abelian.coimageImageComparisonFunctor 📋 Mathlib.CategoryTheory.Abelian.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.Arrow C)
• CategoryTheory.Abelian.coimageImageComparisonFunctor_obj 📋 Mathlib.CategoryTheory.Abelian.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] (f : CategoryTheory.Arrow C) : CategoryTheory.Abelian.coimageImageComparisonFunctor.obj f = CategoryTheory.Arrow.mk (CategoryTheory.Abelian.coimageImageComparison f.hom)
• CategoryTheory.Abelian.coimageImageComparisonFunctor_map 📋 Mathlib.CategoryTheory.Abelian.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {f g : CategoryTheory.Arrow C} (η : f ⟶ g) : CategoryTheory.Abelian.coimageImageComparisonFunctor.map η = CategoryTheory.Arrow.homMk (CategoryTheory.Limits.cokernel.map (CategoryTheory.Limits.kernel.ι f.hom) (CategoryTheory.Limits.kernel.ι g.hom) (CategoryTheory.Limits.kernel.map f.hom g.hom η.left η.right ⋯) η.left ⋯) (CategoryTheory.Limits.kernel.map (CategoryTheory.Limits.cokernel.π f.hom) (CategoryTheory.Limits.cokernel.π g.hom) η.right (CategoryTheory.Limits.cokernel.map f.hom g.hom η.left η.right ⋯) ⋯) ⋯
• ComplexShape.Embedding.restrictionFunctor 📋 Mathlib.Algebra.Homology.Embedding.Restriction
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3) [CategoryTheory.Category.{u_4, u_3} C] [e.IsRelIff] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Functor (HomologicalComplex C c') (HomologicalComplex C c)
• ComplexShape.Embedding.instPreservesZeroMorphismsHomologicalComplexRestrictionFunctor 📋 Mathlib.Algebra.Homology.Embedding.Restriction
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3) [CategoryTheory.Category.{u_4, u_3} C] [e.IsRelIff] [CategoryTheory.Limits.HasZeroMorphisms C] : (e.restrictionFunctor C).PreservesZeroMorphisms
• ComplexShape.Embedding.restrictionFunctor_obj 📋 Mathlib.Algebra.Homology.Embedding.Restriction
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3) [CategoryTheory.Category.{u_4, u_3} C] [e.IsRelIff] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') : (e.restrictionFunctor C).obj K = K.restriction e
• ComplexShape.Embedding.instAdditiveHomologicalComplexRestrictionFunctor 📋 Mathlib.Algebra.Homology.Embedding.Restriction
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3) [CategoryTheory.Category.{u_4, u_3} C] [e.IsRelIff] [CategoryTheory.Preadditive C] : (e.restrictionFunctor C).Additive
• ComplexShape.Embedding.restrictionFunctor.congr_simp 📋 Mathlib.Algebra.Homology.Embedding.Restriction
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e e✝ : c.Embedding c') (e_e : e = e✝) (C : Type u_3) [CategoryTheory.Category.{u_4, u_3} C] [e.IsRelIff] [CategoryTheory.Limits.HasZeroMorphisms C] : e.restrictionFunctor C = e✝.restrictionFunctor C
• ComplexShape.Embedding.restrictionFunctor_map 📋 Mathlib.Algebra.Homology.Embedding.Restriction
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3) [CategoryTheory.Category.{u_4, u_3} C] [e.IsRelIff] [CategoryTheory.Limits.HasZeroMorphisms C] {X✝ Y✝ : HomologicalComplex C c'} (φ : X✝ ⟶ Y✝) : (e.restrictionFunctor C).map φ = HomologicalComplex.restrictionMap φ e
• UniformOnFun 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  (α : Type u_1) (β : Type u_2) : Set (Set α) → Type (max u_1 u_2)
• instNonemptyUniformOnFun 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Nonempty β] : Nonempty (UniformOnFun α β 𝔖)
• instSubsingletonUniformOnFun 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Subsingleton β] : Subsingleton (UniformOnFun α β 𝔖)
• UniformOnFun.ofFun 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)) : (α → β) ≃ UniformOnFun α β 𝔖
• UniformOnFun.toFun 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)) : UniformOnFun α β 𝔖 ≃ (α → β)
• UniformOnFun.topologicalSpace 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  (α : Type u_1) (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) : TopologicalSpace (UniformOnFun α β 𝔖)
• UniformOnFun.uniformSpace 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  (α : Type u_1) (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) : UniformSpace (UniformOnFun α β 𝔖)
• UniformOnFun.instCompleteSpace 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} [CompleteSpace β] : CompleteSpace (UniformOnFun α β 𝔖)
• UniformOnFun.gen 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)) (S : Set α) (V : Set (β × β)) : Set (UniformOnFun α β 𝔖 × UniformOnFun α β 𝔖)
• UniformOnFun.topologicalSpace.eq_1 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  (α : Type u_1) (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) : UniformOnFun.topologicalSpace α β 𝔖 = (UniformOnFun.uniformSpace α β 𝔖).toTopologicalSpace
• UniformOnFun.t2Space_of_covering 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} [T2Space β] (h : ⋃₀ 𝔖 = Set.univ) : T2Space (UniformOnFun α β 𝔖)
• UniformOnFun.congrRight 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} [UniformSpace γ] (e : γ ≃ᵤ β) : UniformOnFun α γ 𝔖 ≃ᵤ UniformOnFun α β 𝔖
• UniformOnFun.uniformEquivUniformFun 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) (h : Set.univ ∈ 𝔖) : UniformOnFun α β 𝔖 ≃ᵤ UniformFun α β
• UniformOnFun.comap_eq 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} {f : γ → β} : UniformOnFun.uniformSpace α γ 𝔖 = UniformSpace.comap (fun x => f ∘ x) (UniformOnFun.uniformSpace α β 𝔖)
• UniformOnFun.iInf_eq 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {γ : Type u_3} {ι : Type u_4} {𝔖 : Set (Set α)} {u : ι → UniformSpace γ} : UniformOnFun.uniformSpace α γ 𝔖 = ⨅ i, UniformOnFun.uniformSpace α γ 𝔖
• UniformOnFun.inf_eq 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {γ : Type u_3} {𝔖 : Set (Set α)} {u₁ u₂ : UniformSpace γ} : UniformOnFun.uniformSpace α γ 𝔖 = UniformOnFun.uniformSpace α γ 𝔖 ⊓ UniformOnFun.uniformSpace α γ 𝔖
• UniformOnFun.uniformEquivPiComm 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {ι : Type u_4} (𝔖 : Set (Set α)) (δ : ι → Type u_5) [(i : ι) → UniformSpace (δ i)] : UniformOnFun α ((i : ι) → δ i) 𝔖 ≃ᵤ ((i : ι) → UniformOnFun α (δ i) 𝔖)
• UniformOnFun.uniformEquivProdArrow 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} [UniformSpace γ] : UniformOnFun α (β × γ) 𝔖 ≃ᵤ UniformOnFun α β 𝔖 × UniformOnFun α γ 𝔖
• UniformOnFun.mono 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {γ : Type u_3} ⦃u₁ u₂ : UniformSpace γ⦄ (hu : u₁ ≤ u₂) ⦃𝔖₁ 𝔖₂ : Set (Set α)⦄ (h𝔖 : 𝔖₂ ⊆ 𝔖₁) : UniformOnFun.uniformSpace α γ 𝔖₁ ≤ UniformOnFun.uniformSpace α γ 𝔖₂
• UniformOnFun.gen_mono 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {S S' : Set α} {V V' : Set (β × β)} (hS : S' ⊆ S) (hV : V ⊆ V') : UniformOnFun.gen 𝔖 S V ⊆ UniformOnFun.gen 𝔖 S' V'
• UniformOnFun.hasBasis_uniformity_of_basis_aux₁ 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  (α : Type u_1) (β : Type u_2) {ι : Type u_4} [UniformSpace β] (𝔖 : Set (Set α)) {p : ι → Prop} {s : ι → Set (β × β)} (hb : (uniformity β).HasBasis p s) (S : Set α) : (uniformity (UniformOnFun α β 𝔖)).HasBasis p fun i => UniformOnFun.gen 𝔖 S (s i)
• UniformOnFun.uniformContinuous_toFun 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} (h : ⋃₀ 𝔖 = Set.univ) : UniformContinuous ⇑(UniformOnFun.toFun 𝔖)
• UniformOnFun.isClosed_setOf_continuous 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} [TopologicalSpace α] (h : Topology.IsCoherentWith 𝔖) : IsClosed {f | Continuous ((UniformOnFun.toFun 𝔖) f)}
• UniformOnFun.uniformContinuous_eval 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} (h : ⋃₀ 𝔖 = Set.univ) (x : α) : UniformContinuous (Function.eval x ∘ ⇑(UniformOnFun.toFun 𝔖))
• UniformOnFun.hasBasis_uniformity_of_basis_aux₂ 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  (α : Type u_1) (β : Type u_2) {ι : Type u_4} [UniformSpace β] (𝔖 : Set (Set α)) (h : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖) {p : ι → Prop} {s : ι → Set (β × β)} (hb : (uniformity β).HasBasis p s) : DirectedOn ((fun s => UniformSpace.comap s.restrict (UniformFun.uniformSpace (↑s) β)) ⁻¹'o GE.ge) 𝔖
• UniformOnFun.uniformContinuous_eval_of_mem_sUnion 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) {x : α} (hx : x ∈ ⋃₀ 𝔖) : UniformContinuous (Function.eval x ∘ ⇑(UniformOnFun.toFun 𝔖))
• UniformOnFun.gen_mem_uniformity 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} (β : Type u_2) {s : Set α} [UniformSpace β] (𝔖 : Set (Set α)) (hs : s ∈ 𝔖) {V : Set (β × β)} (hV : V ∈ uniformity β) : UniformOnFun.gen 𝔖 s V ∈ uniformity (UniformOnFun α β 𝔖)
• UniformOnFun.toFun_ofFun 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} (f : α → β) : (UniformOnFun.toFun 𝔖) ((UniformOnFun.ofFun 𝔖) f) = f
• UniformOnFun.isCountablyGenerated_uniformity 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} [UniformSpace β] (𝔖 : Set (Set α)) [(uniformity β).IsCountablyGenerated] {t : ℕ → Set α} (ht : ∀ (n : ℕ), t n ∈ 𝔖) (hmono : Monotone t) (hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n) : (uniformity (UniformOnFun α β 𝔖)).IsCountablyGenerated
• UniformOnFun.uniformContinuous_eval_of_mem 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} (β : Type u_2) {s : Set α} [UniformSpace β] (𝔖 : Set (Set α)) {x : α} (hxs : x ∈ s) (hs : s ∈ 𝔖) : UniformContinuous (Function.eval x ∘ ⇑(UniformOnFun.toFun 𝔖))
• UniformOnFun.ofFun_toFun 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} (f : UniformOnFun α β 𝔖) : (UniformOnFun.ofFun 𝔖) ((UniformOnFun.toFun 𝔖) f) = f
• UniformOnFun.congrLeft 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} {𝔗 : Set (Set γ)} (e : γ ≃ α) (he : 𝔗 ⊆ Set.image ⇑e ⁻¹' 𝔖) (he' : 𝔖 ⊆ Set.preimage ⇑e ⁻¹' 𝔗) : UniformOnFun γ β 𝔗 ≃ᵤ UniformOnFun α β 𝔖
• UniformOnFun.uniformContinuous_restrict_toFun 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} : UniformContinuous ((⋃₀ 𝔖).restrict ∘ ⇑(UniformOnFun.toFun 𝔖))
• UniformOnFun.uniformContinuous_ofUniformFun 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) : UniformContinuous fun f => (UniformOnFun.ofFun 𝔖) (UniformFun.toFun f)
• UniformOnFun.hasBasis_uniformity_of_basis 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  (α : Type u_1) (β : Type u_2) {ι : Type u_4} [UniformSpace β] (𝔖 : Set (Set α)) (h : 𝔖.Nonempty) (h' : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖) {p : ι → Prop} {s : ι → Set (β × β)} (hb : (uniformity β).HasBasis p s) : (uniformity (UniformOnFun α β 𝔖)).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => UniformOnFun.gen 𝔖 Si.1 (s Si.2)
• UniformOnFun.isBasis_gen 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)) (h : 𝔖.Nonempty) (h' : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖) (𝓑 : FilterBasis (β × β)) : Filter.IsBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓑) fun SV => UniformOnFun.gen 𝔖 SV.1 SV.2
• UniformOnFun.hasAntitoneBasis_uniformity 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} [UniformSpace β] (𝔖 : Set (Set α)) {ι : Type u_5} [Preorder ι] [IsDirected ι fun x1 x2 => x1 ≤ x2] {t : ι → Set α} {V : ι → Set (β × β)} (ht : ∀ (n : ι), t n ∈ 𝔖) (hmono : Monotone t) (hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n) (hb : (uniformity β).HasAntitoneBasis V) : (uniformity (UniformOnFun α β 𝔖)).HasAntitoneBasis fun n => UniformOnFun.gen 𝔖 (t n) (V n)
• UniformOnFun.hasBasis_uniformity 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  (α : Type u_1) (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) (h : 𝔖.Nonempty) (h' : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖) : (uniformity (UniformOnFun α β 𝔖)).HasBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ uniformity β) fun SV => UniformOnFun.gen 𝔖 SV.1 SV.2
• UniformOnFun.hasBasis_uniformity_of_covering_of_basis 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} [UniformSpace β] (𝔖 : Set (Set α)) {ι : Type u_5} {ι' : Type u_6} [Nonempty ι] {t : ι → Set α} {p : ι' → Prop} {V : ι' → Set (β × β)} (ht : ∀ (i : ι), t i ∈ 𝔖) (hdir : Directed (fun x1 x2 => x1 ⊆ x2) t) (hex : ∀ s ∈ 𝔖, ∃ i, s ⊆ t i) (hb : (uniformity β).HasBasis p V) : (uniformity (UniformOnFun α β 𝔖)).HasBasis (fun i => p i.2) fun i => UniformOnFun.gen 𝔖 (t i.1) (V i.2)
• UniformOnFun.precomp_uniformContinuous 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} {𝔗 : Set (Set γ)} {f : γ → α} (hf : Set.MapsTo (fun x => f '' x) 𝔗 𝔖) : UniformContinuous fun g => (UniformOnFun.ofFun 𝔗) ((UniformOnFun.toFun 𝔖) g ∘ f)
• UniformOnFun.postcomp_isUniformEmbedding 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} [UniformSpace γ] {f : γ → β} (hf : IsUniformEmbedding f) : IsUniformEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(UniformOnFun.toFun 𝔖))
• UniformOnFun.postcomp_isUniformInducing 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} [UniformSpace γ] {f : γ → β} (hf : IsUniformInducing f) : IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(UniformOnFun.toFun 𝔖))
• UniformOnFun.postcomp_uniformContinuous 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} [UniformSpace γ] {f : γ → β} (hf : UniformContinuous f) : UniformContinuous (⇑(UniformOnFun.ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(UniformOnFun.toFun 𝔖))
• UniformOnFun.tendsto_iff_tendstoUniformlyOn 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} {p : Filter ι} [UniformSpace β] {𝔖 : Set (Set α)} {F : ι → UniformOnFun α β 𝔖} {f : UniformOnFun α β 𝔖} : Filter.Tendsto F p (nhds f) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (⇑(UniformOnFun.toFun 𝔖) ∘ F) ((UniformOnFun.toFun 𝔖) f) p s
• UniformOnFun.hasBasis_nhds_of_basis 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  (α : Type u_1) (β : Type u_2) {ι : Type u_4} [UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖) (h : 𝔖.Nonempty) (h' : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖) {p : ι → Prop} {s : ι → Set (β × β)} (hb : (uniformity β).HasBasis p s) : (nhds f).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => {g | (g, f) ∈ UniformOnFun.gen 𝔖 Si.1 (s Si.2)}
• UniformOnFun.gen_eq_preimage_restrict 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} (S : Set α) (V : Set (β × β)) : UniformOnFun.gen 𝔖 S V = Prod.map (S.restrict ∘ ⇑UniformFun.toFun) (S.restrict ∘ ⇑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β V
• UniformOnFun.uniformContinuous_ofFun_toFun 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 𝔗 : Set (Set α)) (h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T) : UniformContinuous (⇑(UniformOnFun.ofFun 𝔗) ∘ ⇑(UniformOnFun.toFun 𝔖))
• UniformOnFun.uniformContinuous_restrict 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  (α : Type u_1) (β : Type u_2) {s : Set α} [UniformSpace β] (𝔖 : Set (Set α)) (h : s ∈ 𝔖) : UniformContinuous (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(UniformOnFun.toFun 𝔖))
• UniformOnFun.uniformity_eq_of_basis 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) {ι : Sort u_5} {p : ι → Prop} {V : ι → Set (β × β)} (h : (uniformity β).HasBasis p V) : uniformity (UniformOnFun α β 𝔖) = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), Filter.principal (UniformOnFun.gen 𝔖 s (V i))
• UniformOnFun.hasBasis_nhds 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  (α : Type u_1) (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖) (h : 𝔖.Nonempty) (h' : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖) : (nhds f).HasBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ uniformity β) fun SV => {g | (g, f) ∈ UniformOnFun.gen 𝔖 SV.1 SV.2}
• UniformOnFun.gen.eq_1 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)) (S : Set α) (V : Set (β × β)) : UniformOnFun.gen 𝔖 S V = {uv | ∀ x ∈ S, ((UniformOnFun.toFun 𝔖) uv.1 x, (UniformOnFun.toFun 𝔖) uv.2 x) ∈ V}
• UniformOnFun.continuousAt_eval₂ 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} [TopologicalSpace α] {f : UniformOnFun α β 𝔖} {x : α} (h𝔖 : ∃ V ∈ 𝔖, V ∈ nhds x) (hc : ContinuousAt ((UniformOnFun.toFun 𝔖) f) x) : ContinuousAt (fun fx => (UniformOnFun.toFun 𝔖) fx.1 fx.2) (f, x)
• UniformOnFun.continuous_rng_iff 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} {X : Type u_5} [TopologicalSpace X] {f : X → UniformOnFun α β 𝔖} : Continuous f ↔ ∀ s ∈ 𝔖, Continuous (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(UniformOnFun.toFun 𝔖) ∘ f)
• UniformOnFun.gen_mem_nhds 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} (β : Type u_2) {s : Set α} [UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖) (hs : s ∈ 𝔖) {V : Set (β × β)} (hV : V ∈ uniformity β) : {g | ∀ x ∈ s, ((UniformOnFun.toFun 𝔖) f x, (UniformOnFun.toFun 𝔖) g x) ∈ V} ∈ nhds f
• UniformOnFun.uniformity_eq 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) : uniformity (UniformOnFun α β 𝔖) = ⨅ s ∈ 𝔖, ⨅ V ∈ uniformity β, Filter.principal (UniformOnFun.gen 𝔖 s V)
• UniformOnFun.continuousOn_eval₂ 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} [TopologicalSpace α] (h𝔖 : ∀ (x : α), ∃ V ∈ 𝔖, V ∈ nhds x) : ContinuousOn (fun fx => (UniformOnFun.toFun 𝔖) fx.1 fx.2) {fx | ContinuousAt ((UniformOnFun.toFun 𝔖) fx.1) fx.2}
• UniformOnFun.uniformSpace.eq_1 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  (α : Type u_1) (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) : UniformOnFun.uniformSpace α β 𝔖 = ⨅ s ∈ 𝔖, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) (UniformFun.uniformSpace (↑s) β)
• UniformOnFun.topologicalSpace_eq 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  (α : Type u_1) (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) : UniformOnFun.topologicalSpace α β 𝔖 = ⨅ s ∈ 𝔖, TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) (UniformFun.topologicalSpace (↑s) β)
• UniformOnFun.nhds_eq_of_basis 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) {ι : Sort u_5} {p : ι → Prop} {V : ι → Set (β × β)} (h : (uniformity β).HasBasis p V) (f : UniformOnFun α β 𝔖) : nhds f = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), Filter.principal {g | ∀ x ∈ s, ((UniformOnFun.toFun 𝔖) f x, (UniformOnFun.toFun 𝔖) g x) ∈ V i}
• UniformOnFun.nhds_eq 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖) : nhds f = ⨅ s ∈ 𝔖, ⨅ V ∈ uniformity β, Filter.principal {g | ∀ x ∈ s, ((UniformOnFun.toFun 𝔖) f x, (UniformOnFun.toFun 𝔖) g x) ∈ V}
• UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] (𝔖 : Set (Set α)) {δ : ι → Type u_5} (φ : (i : ι) → δ i → α) (𝔗 : (i : ι) → Set (Set (δ i))) (h_image : ∀ (i : ι), Set.MapsTo (fun x => φ i '' x) (𝔗 i) 𝔖) (h_preimage : ∀ (i : ι), Set.MapsTo (fun x => φ i ⁻¹' x) 𝔖 (𝔗 i)) (h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, Set.range (φ i)) : UniformOnFun.uniformSpace α β 𝔖 = ⨅ i, UniformSpace.comap (⇑(UniformOnFun.ofFun (𝔗 i)) ∘ (fun x => x ∘ φ i) ∘ ⇑(UniformOnFun.toFun 𝔖)) (UniformOnFun.uniformSpace (δ i) β (𝔗 i))
• UniformOnFun.uniformSpace_eq_inf_precomp_of_cover 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} [UniformSpace β] (𝔖 : Set (Set α)) {δ₁ : Type u_5} {δ₂ : Type u_6} (φ₁ : δ₁ → α) (φ₂ : δ₂ → α) (𝔗₁ : Set (Set δ₁)) (𝔗₂ : Set (Set δ₂)) (h_image₁ : Set.MapsTo (fun x => φ₁ '' x) 𝔗₁ 𝔖) (h_image₂ : Set.MapsTo (fun x => φ₂ '' x) 𝔗₂ 𝔖) (h_preimage₁ : Set.MapsTo (fun x => φ₁ ⁻¹' x) 𝔖 𝔗₁) (h_preimage₂ : Set.MapsTo (fun x => φ₂ ⁻¹' x) 𝔖 𝔗₂) (h_cover : ∀ S ∈ 𝔖, S ⊆ Set.range φ₁ ∪ Set.range φ₂) : UniformOnFun.uniformSpace α β 𝔖 = UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔗₁) ∘ (fun x => x ∘ φ₁) ∘ ⇑(UniformOnFun.toFun 𝔖)) (UniformOnFun.uniformSpace δ₁ β 𝔗₁) ⊓ UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔗₂) ∘ (fun x => x ∘ φ₂) ∘ ⇑(UniformOnFun.toFun 𝔖)) (UniformOnFun.uniformSpace δ₂ β 𝔗₂)
• UniformOnFun.isUniformInducing_pi_restrict 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} : IsUniformInducing fun f s => UniformFun.ofFun ((↑s).restrict ((UniformOnFun.toFun 𝔖) f))
• ContinuousMap.toUniformOnFunIsCompact 📋 Mathlib.Topology.UniformSpace.CompactConvergence
  {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] (f : C(α, β)) : UniformOnFun α β {K | IsCompact K}
• ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact 📋 Mathlib.Topology.UniformSpace.CompactConvergence
  {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] : IsUniformEmbedding ContinuousMap.toUniformOnFunIsCompact
• ContinuousMap.range_toUniformOnFunIsCompact 📋 Mathlib.Topology.UniformSpace.CompactConvergence
  {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] : Set.range ContinuousMap.toUniformOnFunIsCompact = {f | Continuous f}
• ContinuousMap.toUniformOnFun_toFun 📋 Mathlib.Topology.UniformSpace.CompactConvergence
  {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] (f : C(α, β)) : (UniformOnFun.toFun {K | IsCompact K}) f.toUniformOnFunIsCompact = ⇑f
• ContinuousMap.continuous_iff_continuous_uniformOnFun 📋 Mathlib.Topology.UniformSpace.CompactConvergence
  {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {X : Type u_1} [TopologicalSpace X] (f : X → C(α, β)) : Continuous f ↔ Continuous fun x => (UniformOnFun.ofFun {K | IsCompact K}) ⇑(f x)
• ContinuousOn.continuous_restrict_iff_continuous_uniformOnFun 📋 Mathlib.Topology.UniformSpace.CompactConvergence
  {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {X : Type u_1} [TopologicalSpace X] {f : X → α → β} {s : Set α} (hf : ∀ (x : X), ContinuousOn (f x) s) [CompactSpace ↑s] : (Continuous fun x => { toFun := s.restrict (f x), continuous_toFun := ⋯ }) ↔ Continuous fun x => (UniformOnFun.ofFun {s}) (f x)
• CategoryTheory.OverPresheafAux.yonedaCollectionFunctor 📋 Mathlib.CategoryTheory.Comma.Presheaf.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) : CategoryTheory.Functor (CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) (CategoryTheory.Functor Cᵒᵖ (Type v))
• CategoryTheory.OverPresheafAux.yonedaCollectionFunctor_obj 📋 Mathlib.CategoryTheory.Comma.Presheaf.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) : (CategoryTheory.OverPresheafAux.yonedaCollectionFunctor A).obj F = CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A F
• CategoryTheory.OverPresheafAux.yonedaCollectionFunctor_map 📋 Mathlib.CategoryTheory.Comma.Presheaf.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) {X✝ Y✝ : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : X✝ ⟶ Y✝) : (CategoryTheory.OverPresheafAux.yonedaCollectionFunctor A).map η = CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁ η
• CategoryTheory.Presheaf.instIsLeftKanExtensionFunctorOppositeTypeIdCompUliftYonedaOfPreservesColimitsOfSizeOfHasPointwiseLeftKanExtension 📋 Mathlib.CategoryTheory.Limits.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [CategoryTheory.Category.{v₂, u₂} ℰ] (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) ℰ) [CategoryTheory.Limits.PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂, max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂} L] [CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension (CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L)] : L.IsLeftKanExtension (CategoryTheory.CategoryStruct.id (CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L))
• CategoryTheory.Presheaf.instIsLeftKanExtensionFunctorOppositeTypeLanOpHomCompULiftYonedaIsoULiftYonedaCompLan 📋 Mathlib.CategoryTheory.Limits.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [∀ (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))), F.op.HasLeftKanExtension P] : F.op.lan.IsLeftKanExtension (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan F).hom
• CategoryTheory.Presheaf.instUniqueHomLeftExtensionFunctorOppositeTypeUliftYonedaCompMkLanOpHomCompULiftYonedaIsoULiftYonedaCompLan 📋 Mathlib.CategoryTheory.Limits.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [∀ (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))), F.op.HasLeftKanExtension P] (Φ : CategoryTheory.StructuredArrow (F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂}) ((CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) (CategoryTheory.Functor Dᵒᵖ (Type (max w v₁ v₂)))).obj CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁})) : Unique (CategoryTheory.Functor.LeftExtension.mk F.op.lan (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶ Φ)
• CategoryTheory.Functor.mapCommMonFunctor 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] : CategoryTheory.Functor (CategoryTheory.LaxBraidedFunctor C D) (CategoryTheory.Functor (CommMon C) (CommMon D))
• CategoryTheory.Functor.mapCommMonFunctor_obj 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (F : CategoryTheory.LaxBraidedFunctor C D) : (CategoryTheory.Functor.mapCommMonFunctor C D).obj F = F.mapCommMon
• CategoryTheory.Functor.mapCommMonFunctor_map_app_hom 📋 Mathlib.CategoryTheory.Monoidal.CommMon_
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {X✝ Y✝ : CategoryTheory.LaxBraidedFunctor C D} (α : X✝ ⟶ Y✝) (A : CommMon C) : (((CategoryTheory.Functor.mapCommMonFunctor C D).map α).app A).hom = α.hom.app A.X
• instFaithfulMonFunctorOppositeMonCatYonedaMon 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] : yonedaMon.Faithful
• instFullMonFunctorOppositeMonCatYonedaMon 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.CartesianMonoidalCategory C] : yonedaMon.Full
• CategoryTheory.GrothendieckTopology.instIsLocalizationFunctorOppositeSheafPresheafToSheafW 📋 Mathlib.CategoryTheory.Sites.Localization
  {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_2} [CategoryTheory.Category.{u_4, u_2} A] [CategoryTheory.HasWeakSheafify J A] : (CategoryTheory.presheafToSheaf J A).IsLocalization J.W
• instAddCommGroupUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [AddCommGroup β] : AddCommGroup (UniformOnFun α β 𝔖)
• instAddCommMonoidUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [AddCommMonoid β] : AddCommMonoid (UniformOnFun α β 𝔖)
• instAddGroupUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [AddGroup β] : AddGroup (UniformOnFun α β 𝔖)
• instAddMonoidUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [AddMonoid β] : AddMonoid (UniformOnFun α β 𝔖)
• instAddUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Add β] : Add (UniformOnFun α β 𝔖)
• instCommGroupUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [CommGroup β] : CommGroup (UniformOnFun α β 𝔖)
• instCommMonoidUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [CommMonoid β] : CommMonoid (UniformOnFun α β 𝔖)
• instDivUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Div β] : Div (UniformOnFun α β 𝔖)
• instGroupUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Group β] : Group (UniformOnFun α β 𝔖)
• instInvUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Inv β] : Inv (UniformOnFun α β 𝔖)
• instMonoidUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Monoid β] : Monoid (UniformOnFun α β 𝔖)
• instMulUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Mul β] : Mul (UniformOnFun α β 𝔖)
• instNegUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Neg β] : Neg (UniformOnFun α β 𝔖)
• instOneUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [One β] : One (UniformOnFun α β 𝔖)
• instSubUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Sub β] : Sub (UniformOnFun α β 𝔖)
• instZeroUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Zero β] : Zero (UniformOnFun α β 𝔖)
• instSMulUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [SMul M β] : SMul M (UniformOnFun α β 𝔖)
• instMulActionUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [Monoid M] [MulAction M β] : MulAction M (UniformOnFun α β 𝔖)
• instAddCommGroupUniformOnFun.eq_1 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [AddCommGroup β] : instAddCommGroupUniformOnFun = Pi.addCommGroup
• instAddCommMonoidUniformOnFun.eq_1 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [AddCommMonoid β] : instAddCommMonoidUniformOnFun = Pi.addCommMonoid
• instAddGroupUniformOnFun.eq_1 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [AddGroup β] : instAddGroupUniformOnFun = Pi.addGroup
• instAddMonoidUniformOnFun.eq_1 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [AddMonoid β] : instAddMonoidUniformOnFun = Pi.addMonoid
• instAddUniformOnFun.eq_1 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Add β] : instAddUniformOnFun = Pi.instAdd
• instCommGroupUniformOnFun.eq_1 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [CommGroup β] : instCommGroupUniformOnFun = Pi.commGroup
• instCommMonoidUniformOnFun.eq_1 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [CommMonoid β] : instCommMonoidUniformOnFun = Pi.commMonoid
• instDivUniformOnFun.eq_1 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Div β] : instDivUniformOnFun = Pi.instDiv
• instGroupUniformOnFun.eq_1 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Group β] : instGroupUniformOnFun = Pi.group
• instInvUniformOnFun.eq_1 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Inv β] : instInvUniformOnFun = Pi.instInv
• instMonoidUniformOnFun.eq_1 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Monoid β] : instMonoidUniformOnFun = Pi.monoid
• instMulUniformOnFun.eq_1 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Mul β] : instMulUniformOnFun = Pi.instMul
• instNegUniformOnFun.eq_1 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Neg β] : instNegUniformOnFun = Pi.instNeg
• instOneUniformOnFun.eq_1 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [One β] : instOneUniformOnFun = Pi.instOne
• instSubUniformOnFun.eq_1 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Sub β] : instSubUniformOnFun = Pi.instSub
• instZeroUniformOnFun.eq_1 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Zero β] : instZeroUniformOnFun = Pi.instZero
• instDistribMulActionUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [Monoid M] [AddMonoid β] [DistribMulAction M β] : DistribMulAction M (UniformOnFun α β 𝔖)
• instModuleUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {R : Type u_4} {𝔖 : Set (Set α)} [Semiring R] [AddCommMonoid β] [Module R β] : Module R (UniformOnFun α β 𝔖)
• instIsUniformAddGroupUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {G : Type u_2} [AddGroup G] {𝔖 : Set (Set α)} [UniformSpace G] [IsUniformAddGroup G] : IsUniformAddGroup (UniformOnFun α G 𝔖)
• instIsUniformGroupUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {G : Type u_2} [Group G] {𝔖 : Set (Set α)} [UniformSpace G] [IsUniformGroup G] : IsUniformGroup (UniformOnFun α G 𝔖)
• instSMulCommClassUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} {N : Type u_6} [SMul M β] [SMul N β] [SMulCommClass M N β] : SMulCommClass M N (UniformOnFun α β 𝔖)
• instIsScalarTowerUniformOnFun 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} {N : Type u_6} [SMul M N] [SMul M β] [SMul N β] [IsScalarTower M N β] : IsScalarTower M N (UniformOnFun α β 𝔖)
• UniformOnFun.one_apply 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [One β] : (UniformOnFun.ofFun 𝔖) 1 = 1
• UniformOnFun.toFun_one 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [One β] : (UniformOnFun.toFun 𝔖) 1 = 1
• UniformOnFun.toFun_zero 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Zero β] : (UniformOnFun.toFun 𝔖) 0 = 0
• UniformOnFun.zero_apply 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Zero β] : (UniformOnFun.ofFun 𝔖) 0 = 0
• UniformOnFun.ofFun_inv 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Inv β] (f : α → β) : (UniformOnFun.ofFun 𝔖) f⁻¹ = ((UniformOnFun.ofFun 𝔖) f)⁻¹
• UniformOnFun.ofFun_neg 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Neg β] (f : α → β) : (UniformOnFun.ofFun 𝔖) (-f) = -(UniformOnFun.ofFun 𝔖) f
• UniformOnFun.toFun_inv 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Inv β] (f : UniformOnFun α β 𝔖) : (UniformOnFun.toFun 𝔖) f⁻¹ = ((UniformOnFun.toFun 𝔖) f)⁻¹
• UniformOnFun.toFun_neg 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Neg β] (f : UniformOnFun α β 𝔖) : (UniformOnFun.toFun 𝔖) (-f) = -(UniformOnFun.toFun 𝔖) f
• UniformOnFun.ofFun_prod 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {ι : Type u_3} {𝔖 : Set (Set α)} {β : Type u_4} [CommMonoid β] {f : ι → α → β} (I : Finset ι) : (UniformOnFun.ofFun 𝔖) (∏ i ∈ I, f i) = ∏ i ∈ I, (UniformOnFun.ofFun 𝔖) (f i)
• UniformOnFun.ofFun_sum 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {ι : Type u_3} {𝔖 : Set (Set α)} {β : Type u_4} [AddCommMonoid β] {f : ι → α → β} (I : Finset ι) : (UniformOnFun.ofFun 𝔖) (∑ i ∈ I, f i) = ∑ i ∈ I, (UniformOnFun.ofFun 𝔖) (f i)
• UniformOnFun.toFun_prod 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {ι : Type u_3} {𝔖 : Set (Set α)} {β : Type u_4} [CommMonoid β] {f : ι → α → β} (I : Finset ι) : (UniformOnFun.toFun 𝔖) (∏ i ∈ I, f i) = ∏ i ∈ I, (UniformOnFun.toFun 𝔖) (f i)
• UniformOnFun.toFun_sum 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {ι : Type u_3} {𝔖 : Set (Set α)} {β : Type u_4} [AddCommMonoid β] {f : ι → α → β} (I : Finset ι) : (UniformOnFun.toFun 𝔖) (∑ i ∈ I, f i) = ∑ i ∈ I, (UniformOnFun.toFun 𝔖) (f i)
• UniformOnFun.ofFun_smul 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [SMul M β] (c : M) (f : α → β) : (UniformOnFun.ofFun 𝔖) (c • f) = c • (UniformOnFun.ofFun 𝔖) f
• UniformOnFun.toFun_smul 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [SMul M β] (c : M) (f : UniformOnFun α β 𝔖) : (UniformOnFun.toFun 𝔖) (c • f) = c • (UniformOnFun.toFun 𝔖) f
• UniformOnFun.hasBasis_nhds_one 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {G : Type u_2} [Group G] [UniformSpace G] [IsUniformGroup G] (𝔖 : Set (Set α)) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖) : (nhds 1).HasBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ nhds 1) fun SV => {f | ∀ x ∈ SV.1, f x ∈ SV.2}
• UniformOnFun.hasBasis_nhds_zero 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {G : Type u_2} [AddGroup G] [UniformSpace G] [IsUniformAddGroup G] (𝔖 : Set (Set α)) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖) : (nhds 0).HasBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ nhds 0) fun SV => {f | ∀ x ∈ SV.1, f x ∈ SV.2}
• UniformOnFun.ofFun_add 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Add β] (f g : α → β) : (UniformOnFun.ofFun 𝔖) (f + g) = (UniformOnFun.ofFun 𝔖) f + (UniformOnFun.ofFun 𝔖) g
• UniformOnFun.ofFun_div 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Div β] (f g : α → β) : (UniformOnFun.ofFun 𝔖) (f / g) = (UniformOnFun.ofFun 𝔖) f / (UniformOnFun.ofFun 𝔖) g
• UniformOnFun.ofFun_mul 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Mul β] (f g : α → β) : (UniformOnFun.ofFun 𝔖) (f * g) = (UniformOnFun.ofFun 𝔖) f * (UniformOnFun.ofFun 𝔖) g
• UniformOnFun.ofFun_sub 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Sub β] (f g : α → β) : (UniformOnFun.ofFun 𝔖) (f - g) = (UniformOnFun.ofFun 𝔖) f - (UniformOnFun.ofFun 𝔖) g
• UniformOnFun.toFun_add 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Add β] (f g : UniformOnFun α β 𝔖) : (UniformOnFun.toFun 𝔖) (f + g) = (UniformOnFun.toFun 𝔖) f + (UniformOnFun.toFun 𝔖) g
• UniformOnFun.toFun_div 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Div β] (f g : UniformOnFun α β 𝔖) : (UniformOnFun.toFun 𝔖) (f / g) = (UniformOnFun.toFun 𝔖) f / (UniformOnFun.toFun 𝔖) g
• UniformOnFun.toFun_mul 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Mul β] (f g : UniformOnFun α β 𝔖) : (UniformOnFun.toFun 𝔖) (f * g) = (UniformOnFun.toFun 𝔖) f * (UniformOnFun.toFun 𝔖) g
• UniformOnFun.toFun_sub 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Sub β] (f g : UniformOnFun α β 𝔖) : (UniformOnFun.toFun 𝔖) (f - g) = (UniformOnFun.toFun 𝔖) f - (UniformOnFun.toFun 𝔖) g
• UniformOnFun.hasBasis_nhds_one_of_basis 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {G : Type u_2} {ι : Type u_3} [Group G] [UniformSpace G] [IsUniformGroup G] (𝔖 : Set (Set α)) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖) {p : ι → Prop} {b : ι → Set G} (h : (nhds 1).HasBasis p b) : (nhds 1).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => {f | ∀ x ∈ Si.1, (UniformOnFun.toFun 𝔖) f x ∈ b Si.2}
• UniformOnFun.hasBasis_nhds_zero_of_basis 📋 Mathlib.Topology.Algebra.UniformConvergence
  {α : Type u_1} {G : Type u_2} {ι : Type u_3} [AddGroup G] [UniformSpace G] [IsUniformAddGroup G] (𝔖 : Set (Set α)) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖) {p : ι → Prop} {b : ι → Set G} (h : (nhds 0).HasBasis p b) : (nhds 0).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => {f | ∀ x ∈ Si.1, (UniformOnFun.toFun 𝔖) f x ∈ b Si.2}
• UniformOnFun.continuousSMul_induced_of_image_bounded 📋 Mathlib.Topology.Algebra.Module.UniformConvergence
  (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) (H : Type u_4) {hom : Type u_5} [NormedField 𝕜] [AddCommGroup H] [Module 𝕜 H] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace H] [UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜 E] {𝔖 : Set (Set α)} [FunLike hom H (α → E)] [LinearMapClass hom 𝕜 H (α → E)] (φ : hom) (hφ : Topology.IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ ⇑φ)) (h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)) : ContinuousSMul 𝕜 H
• UniformOnFun.continuousSMul_submodule_of_image_bounded 📋 Mathlib.Topology.Algebra.Module.UniformConvergence
  (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜 E] {𝔖 : Set (Set α)} (H : Submodule 𝕜 (UniformOnFun α E 𝔖)) (h : ∀ u ∈ H, ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (u '' s)) : ContinuousSMul 𝕜 ↥H
• ContinuousLinearMap.isUniformEmbedding_toUniformOnFun 📋 Mathlib.Topology.Algebra.Module.StrongTopology
  {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [UniformSpace F] [IsUniformAddGroup F] : IsUniformEmbedding fun f => (UniformOnFun.ofFun {s | Bornology.IsVonNBounded 𝕜₁ s}) ⇑f
• ContinuousMultilinearMap.toUniformOnFun 📋 Mathlib.Topology.Algebra.Module.Multilinear.Topology
  {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : ContinuousMultilinearMap 𝕜 E F) : UniformOnFun ((i : ι) → E i) F {s | Bornology.IsVonNBounded 𝕜 s}
• ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun 📋 Mathlib.Topology.Algebra.Module.Multilinear.Topology
  {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [IsUniformAddGroup F] : IsUniformEmbedding ContinuousMultilinearMap.toUniformOnFun
• ContinuousMultilinearMap.isUniformInducing_toUniformOnFun 📋 Mathlib.Topology.Algebra.Module.Multilinear.Topology
  {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [IsUniformAddGroup F] : IsUniformInducing ContinuousMultilinearMap.toUniformOnFun
• ContinuousMultilinearMap.isEmbedding_toUniformOnFun 📋 Mathlib.Topology.Algebra.Module.Multilinear.Topology
  {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [IsUniformAddGroup F] : Topology.IsEmbedding ContinuousMultilinearMap.toUniformOnFun
• ContinuousMultilinearMap.toUniformOnFun_toFun 📋 Mathlib.Topology.Algebra.Module.Multilinear.Topology
  {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : ContinuousMultilinearMap 𝕜 E F) : (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f.toUniformOnFun = ⇑f
• ContinuousMultilinearMap.range_toUniformOnFun 📋 Mathlib.Topology.Algebra.Module.Multilinear.Topology
  {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [DecidableEq ι] [TopologicalSpace F] : Set.range ContinuousMultilinearMap.toUniformOnFun = {f | Continuous ((UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f) ∧ (∀ (m : (i : ι) → E i) (i : ι) (x y : E i), (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i (x + y)) = (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i x) + (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i y)) ∧ ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i), (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i (c • x)) = c • (UniformOnFun.toFun {s | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i x)}
• UniformOnFun.instEDistOfFiniteElemSet 📋 Mathlib.Topology.MetricSpace.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [PseudoEMetricSpace β] [Finite ↑𝔖] : EDist (UniformOnFun α β 𝔖)
• UniformOnFun.instPseudoEMetricSpace 📋 Mathlib.Topology.MetricSpace.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [PseudoEMetricSpace β] [Finite ↑𝔖] : PseudoEMetricSpace (UniformOnFun α β 𝔖)
• UniformOnFun.instPseudoMetricSpaceOfBoundedSpace 📋 Mathlib.Topology.MetricSpace.UniformConvergence
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Finite ↑𝔖] [PseudoMetricSpace β] [BoundedSpace β] : PseudoMetricSpace (UniformOnFun α β 𝔖)

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 187ba29 serving mathlib revision 6c19380