Loogle!
Result
Found 337 declarations whose name contains "onFun". Of these, only the first 200 are shown.
- Lean.ProjectionFunctionInfo π Lean.ProjFns
: Type - 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.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 - Function.onFun π Mathlib.Logic.Function.Defs
{Ξ± : Sort uβ} {Ξ² : Sort uβ} {Ο : Sort uβ} (f : Ξ² β Ξ² β Ο) (g : Ξ± β Ξ²) : Ξ± β Ξ± β Ο - 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 - 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) - 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.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_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.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.instIsLeftKanExtensionFunctorOppositeTypeIdCompYonedaOfPreservesColimitsOfSizeOfHasPointwiseLeftKanExtension π 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 vβ)) β°) [CategoryTheory.Limits.PreservesColimitsOfSize.{vβ, max uβ vβ, max uβ vβ, vβ, max uβ (vβ + 1), uβ} L] [CategoryTheory.yoneda.HasPointwiseLeftKanExtension (CategoryTheory.yoneda.comp L)] : L.IsLeftKanExtension (CategoryTheory.CategoryStruct.id (CategoryTheory.yoneda.comp L)) - CategoryTheory.Presheaf.instIsLeftKanExtensionFunctorOppositeTypeLanOpHomCompYonedaIsoYonedaCompLan π 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 vβ)), F.op.HasLeftKanExtension P] : F.op.lan.IsLeftKanExtension (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan F).hom - CategoryTheory.Presheaf.instUniqueHomLeftExtensionFunctorOppositeTypeYonedaCompMkLanOpHomCompYonedaIsoYonedaCompLan π 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 vβ)), F.op.HasLeftKanExtension P] (Ξ¦ : CategoryTheory.StructuredArrow (F.comp CategoryTheory.yoneda) ((CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Functor Cα΅α΅ (Type vβ)) (CategoryTheory.Functor Dα΅α΅ (Type vβ))).obj CategoryTheory.yoneda)) : Unique (CategoryTheory.Functor.LeftExtension.mk F.op.lan (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan 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 - 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.embedding_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.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 Ξ± Ξ² π) - UniformOnFun.instBoundedSpace π Mathlib.Topology.MetricSpace.UniformConvergence
{Ξ± : Type u_1} {Ξ² : Type u_2} {π : Set (Set Ξ±)} [Finite βπ] [PseudoMetricSpace Ξ²] [BoundedSpace Ξ²] : BoundedSpace (UniformOnFun Ξ± Ξ² π) - UniformOnFun.lipschitzWith_eval π Mathlib.Topology.MetricSpace.UniformConvergence
{Ξ± : Type u_1} {Ξ² : Type u_2} {π : Set (Set Ξ±)} [PseudoEMetricSpace Ξ²] [Finite βπ] {x : Ξ±} (hx : x β ββ π) : LipschitzWith 1 fun f => (UniformOnFun.toFun π) f x - UniformOnFun.lipschitzWith_iff π Mathlib.Topology.MetricSpace.UniformConvergence
{Ξ± : Type u_1} {Ξ² : Type u_2} {Ξ³ : Type u_3} [PseudoEMetricSpace Ξ³] {π : Set (Set Ξ±)} [PseudoEMetricSpace Ξ²] [Finite βπ] {f : Ξ³ β UniformOnFun Ξ± Ξ² π} {K : NNReal} : LipschitzWith K f β β c β ββ π, LipschitzWith K fun x => (UniformOnFun.toFun π) (f x) c - UniformOnFun.lipschitzOnWith_iff π Mathlib.Topology.MetricSpace.UniformConvergence
{Ξ± : Type u_1} {Ξ² : Type u_2} {Ξ³ : Type u_3} [PseudoEMetricSpace Ξ³] {π : Set (Set Ξ±)} [PseudoEMetricSpace Ξ²] [Finite βπ] {f : Ξ³ β UniformOnFun Ξ± Ξ² π} {K : NNReal} {s : Set Ξ³} : LipschitzOnWith K f s β β c β ββ π, LipschitzOnWith K (fun x => (UniformOnFun.toFun π) (f x) c) s - UniformOnFun.continuous_of_forall_lipschitzWith π Mathlib.Topology.MetricSpace.UniformConvergence
{Ξ± : Type u_1} {Ξ² : Type u_2} {Ξ³ : Type u_3} [PseudoEMetricSpace Ξ³] {π : Set (Set Ξ±)} [PseudoEMetricSpace Ξ²] {f : Ξ³ β UniformOnFun Ξ± Ξ² π} (K : Set Ξ± β NNReal) (h : β s β π, β c β s, LipschitzWith (K s) fun x => (UniformOnFun.toFun π) (f x) c) : Continuous f - UniformOnFun.lipschitzWith_one_ofFun_toFun π Mathlib.Topology.MetricSpace.UniformConvergence
{Ξ± : Type u_1} {Ξ² : Type u_2} {π : Set (Set Ξ±)} [PseudoEMetricSpace Ξ²] [Finite βπ] : LipschitzWith 1 (β(UniformOnFun.ofFun π) β βUniformFun.toFun) - UniformOnFun.edist_eval_le π Mathlib.Topology.MetricSpace.UniformConvergence
{Ξ± : Type u_1} {Ξ² : Type u_2} {π : Set (Set Ξ±)} [PseudoEMetricSpace Ξ²] [Finite βπ] {f g : UniformOnFun Ξ± Ξ² π} {x : Ξ±} (hx : x β ββ π) : edist ((UniformOnFun.toFun π) f x) ((UniformOnFun.toFun π) g x) β€ edist f g
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. You can also try the
#loogle
command from LeanSearchClient,
the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
πReal.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
π"differ"
finds all lemmas that have"differ"
somewhere in their lemma name.By subexpression:
π_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
πReal.sqrt ?a * Real.sqrt ?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
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 findtsum_lt_tsum
even though the hypothesisf 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 ba454ce