Topology

📁 Source: Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean

Statistics

Metric	Count
Definitions apply, instTopologicalSpace, instUniformSpace, restrictScalarsLinear, toUniformOnFun	5
Theorems apply_apply, completeSpace, continuous_restrictScalars, hasBasis_nhds_zero, hasBasis_nhds_zero_of_basis, hasSum_eval, instCompleteSpace, instContinuousConstSMul, instContinuousEvalConstForall, instContinuousSMul, instIsTopologicalAddGroup, instIsUniformAddGroup, instT2Space, instT3Space, instUniformContinuousConstSMul, isEmbedding_restrictScalars, isEmbedding_toUniformOnFun, isUniformEmbedding_restrictScalars, isUniformEmbedding_toUniformOnFun, isUniformInducing_postcomp, isUniformInducing_toUniformOnFun, range_toUniformOnFun, restrictScalarsLinear_apply, toUniformOnFun_toFun, tsum_eval, uniformContinuous_coe_fun, uniformContinuous_eval_const, uniformContinuous_restrictScalars	28
Total	33

ContinuousMultilinearMap

Definitions

Name	Category	Theorems
apply 📖	CompOp	5 math math: HasFDerivWithinAt.continuousMultilinearMap_apply, apply_apply, HasStrictFDerivAt.continuousMultilinearMap_apply, hasStrictFDerivAt_uncurry, HasFDerivAt.continuousMultilinearMap_apply
instTopologicalSpace 📖	CompOp	146 math math: fderiv_iteratedFDeriv, ContinuousAlternatingMap.isClosedEmbedding_toContinuousMultilinearMap, FormalMultilinearSeries.changeOriginSeries_sum_eq_partialSum_of_finite, norm_iteratedFDerivComponent_le, ContinuousAlternatingMap.hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff, hasFTaylorSeriesUpToOn_top_iff_right, FormalMultilinearSeries.changeOriginSeriesTerm_apply, HasFTaylorSeriesUpTo.cont, MultilinearMap.mkContinuousMultilinear_apply, norm_compContinuousLinearMapLRight_le, ContinuousAlternatingMap.isClosed_range_toContinuousMultilinearMap, FormalMultilinearSeries.changeOriginSeries_summable_aux₃, HasFDerivWithinAt.linear_multilinear_comp, iteratedFDerivWithin_succ_eq_comp_left, contDiffOn_iff_continuousOn_differentiableOn, PiTensorProduct.toDualContinuousMultilinearMap_apply_apply, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_apply_le, norm_smulRightL_le, ContinuousLinearMap.cpolynomialOn_uncurry_of_multilinear, VectorFourier.fourierPowSMulRight_eq_comp, ContinuousLinearMap.hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear, ContinuousLinearMap.flipMultilinear_apply_apply, uncurrySum_apply, isEmbedding_restrictScalars, FormalMultilinearSeries.nnnorm_changeOriginSeries_le_tsum, ContDiffWithinAt.continuousWithinAt_iteratedFDerivWithin, ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap, curryFinFinset_symm_apply_const, curryLeft_norm, ContDiffOn.continuousOn_iteratedFDerivWithin, HasFTaylorSeriesUpToOn.cont, restrictScalarsLinear_apply, contDiffOn_nat_iff_continuousOn_differentiableOn, ContDiff.differentiable_iteratedFDeriv, ContinuousLinearMap.analyticWithinAt_uncurry_of_multilinear, FormalMultilinearSeries.iteratedFDerivSeries_eq_zero, hasBasis_nhds_zero, FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm_apply_le, hasFTaylorSeriesUpToOn_top_iff', iteratedFDeriv_tsum, ContinuousLinearMap.cpolyomialOn_uncurry_of_multilinear, contDiff_iff_continuous_differentiable, hasFTaylorSeriesUpToOn_succ_iff_right, ContinuousLinearMap.coe_flipMultilinearEquiv, FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum, hasFTaylorSeriesUpTo_top_iff', fderivWithin_iteratedFDerivWithin, instContinuousEvalConstForall, MultilinearMap.mkContinuousLinear_norm_le, ContinuousLinearMap.uncurryLeft_apply, curryFinFinset_apply_const, compContinuousLinearMapLRight_apply, ContinuousLinearMap.continuousMultilinearMapOption_apply_eq_self, apply_apply, flipLinear_apply_apply, hasFTaylorSeriesUpTo_succ_nat_iff_right, ContinuousLinearMap.cpolynomialAt_uncurry_of_multilinear, hasFTaylorSeriesUpToOn_succ_nat_iff_right, ContinuousAlternatingMap.toContinuousMultilinearMapCLM_apply, instContinuousConstSMul, ContinuousLinearMap.continuousWithinAt_uncurry_of_multilinear, PiTensorProduct.dualSeminorms_bounded, curryMidEquiv_apply, ContinuousOn.continuousOn_iteratedFDerivWithin, iteratedFDerivWithin_succ_apply_left, instContinuousEval, HasFTaylorSeriesUpToOn.fderivWithin, ContinuousLinearMap.norm_map_tail_le, PiTensorProduct.injectiveSeminorm_apply, norm_fderiv_iteratedFDeriv, MultilinearMap.mkContinuousLinear_norm_le', norm_fderivWithin_iteratedFDerivWithin, ContinuousLinearEquiv.continuousMultilinearMapCongrRight_symm, ContinuousAlternatingMap.toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap, ContinuousLinearMap.norm_uncurryMid, ContinuousLinearMap.uncurryLeft_norm, MeasureTheory.AEStronglyMeasurable.fourierPowSMulRight, ContDiff.continuous_iteratedFDeriv', ContinuousLinearMap.continuous_uncurry_of_multilinear, ContDiffMapSupportedIn.isUniformEmbedding_pi_structureMapCLM, isEmbedding_toUniformOnFun, MultilinearMap.mkContinuousMultilinear_norm_le', curryFinFinset_symm_apply_piecewise_const, ContinuousAlternatingMap.toContinuousMultilinearMap_curryLeft, ContinuousLinearMap.analyticOnNhd_uncurry_of_multilinear, OrderedFinpartition.compAlongOrderedFinpartitionL_apply, instT3Space, ContinuousLinearMap.uncurryMid_apply, continuousMultilinearCurryLeftEquiv_apply, iteratedFDerivComponent_apply, ContDiffWithinAt.differentiableWithinAt_iteratedFDerivWithin, changeOriginSeries_support, ContinuousLinearMap.continuousOn_uncurry_of_multilinear, ContDiff.continuous_iteratedFDeriv, hasBasis_nhds_zero_of_basis, contDiff_nat_iff_continuous_differentiable, MultilinearMap.mkContinuousMultilinear_norm_le, hasStrictFDerivAt_compContinuousLinearMap, curryMid_apply, PiTensorProduct.toDualContinuousMultilinearMap_le_projectiveSeminorm, ContinuousLinearMap.hasFDerivAt_uncurry_of_multilinear, instT2Space, HasFDerivAt.linear_multilinear_comp, ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply, compContinuousLinearMapL_apply, instContinuousSMul, hasFTaylorSeriesUpToOn_succ_iff_left, curryLeft_apply, ContinuousLinearMap.analyticOn_uncurry_of_multilinear, ContinuousLinearMap.coe_symm_flipMultilinearEquiv, Continuous.fourierPowSMulRight, currySum_apply, ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply, FormalMultilinearSeries.changeOriginSeries_finite_of_finite, continuousMultilinearCurryLeftEquiv_symm_apply, smulRightL_apply, iteratedFDeriv_succ_eq_comp_left, ContDiffAt.continuousAt_iteratedFDeriv, ContDiffAt.differentiableAt_iteratedFDeriv, ContinuousOn.continuousOn_iteratedFDeriv, ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_symm, FormalMultilinearSeries.norm_changeOriginSeriesTerm, fderivCompContinuousLinearMap_apply, curryFinFinset_symm_apply, HasFTaylorSeriesUpTo.fderiv, FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm, ContDiffOn.differentiableOn_iteratedFDerivWithin, norm_compContinuousLinearMapL_le, FormalMultilinearSeries.changeOriginSeriesTerm_changeOriginIndexEquiv_symm, VectorFourier.integrable_fourierPowSMulRight, ContinuousAlternatingMap.continuous_toContinuousMultilinearMap, ContinuousLinearMap.analyticAt_uncurry_of_multilinear, iteratedFDeriv_tsum_apply, instIsTopologicalAddGroup, curryFinFinset_apply, FormalMultilinearSeries.changeOriginSeriesTerm_bound, ContinuousLinearMap.norm_map_removeNth_le, hasStrictFDerivAt_uncurry, compContinuousLinearMapContinuousMultilinear_apply_apply, norm_curryMid, continuous_restrictScalars, PiTensorProduct.injectiveSeminorm_def, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_le, ContinuousLinearMap.continuousAt_uncurry_of_multilinear, curryMidEquiv_symm_apply, iteratedFDeriv_succ_apply_left
instUniformSpace 📖	CompOp	14 math math: ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMap, uniformContinuous_eval_const, completeSpace, instIsUniformAddGroup, isUniformEmbedding_toUniformOnFun, uniformContinuous_restrictScalars, instCompleteSpace, ContinuousAlternatingMap.uniformContinuous_toContinuousMultilinearMap, uniformContinuous_coe_fun, instUniformContinuousConstSMul, isUniformInducing_postcomp, SeparatingDual.completeSpace_continuousMultilinearMap_iff, isUniformInducing_toUniformOnFun, isUniformEmbedding_restrictScalars
restrictScalarsLinear 📖	CompOp	1 math math: restrictScalarsLinear_apply
toUniformOnFun 📖	CompOp	5 math math: range_toUniformOnFun, isUniformEmbedding_toUniformOnFun, isEmbedding_toUniformOnFun, toUniformOnFun_toFun, isUniformInducing_toUniformOnFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_apply 📖	mathematical	ContinuousSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap instTopologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.funLike apply funLike	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
completeSpace 📖	mathematical	ContinuousSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Topology.IsCoherentWith Pi.topologicalSpace setOf Set Bornology.IsVonNBounded Pi.instSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Pi.instZero	CompleteSpace ContinuousMultilinearMap instUniformSpace	—	UniformContinuous.continuous UniformOnFun.uniformContinuous_eval Bornology.sUnion_isVonNBounded_eq_univ instContinuousSMulForall completeSpace_iff_isComplete_range isUniformInducing_toUniformOnFun range_toUniformOnFun Set.setOf_forall IsClosed.isComplete UniformOnFun.instCompleteSpace IsClosed.inter UniformOnFun.isClosed_setOf_continuous isClosed_iInter isClosed_eq Continuous.add IsTopologicalAddGroup.toContinuousAdd IsUniformAddGroup.to_topologicalAddGroup Continuous.const_smul SeparationQuotient.instIsUniformAddGroup IsUniformInducing.completeSpace_congr isUniformInducing_postcomp ContinuousLinearMap.compContinuousMultilinearMap_coe SeparationQuotient.mk_outCLM SeparationQuotient.instContinuousConstSMul SeparationQuotient.instCompleteSpace SeparationQuotient.t2Space instR1Space IsTopologicalAddGroup.regularSpace
continuous_restrictScalars 📖	mathematical	ContinuousSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing IsScalarTower Algebra.toSMul Semifield.toCommSemiring NontriviallyNormedField.toNormedField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra	Continuous ContinuousMultilinearMap instTopologicalSpace restrictScalars	—	Topology.IsEmbedding.continuous isEmbedding_restrictScalars
hasBasis_nhds_zero 📖	mathematical	—	Filter.HasBasis ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid Set nhds instTopologicalSpace instZero Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Pi.instSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Pi.instZero Pi.topologicalSpace Filter Filter.instMembership setOf Set.MapsTo DFunLike.coe funLike	—	hasBasis_nhds_zero_of_basis Filter.basis_sets
hasBasis_nhds_zero_of_basis 📖	mathematical	Filter.HasBasis nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid Set instTopologicalSpace instZero Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Pi.instSMul SMulZeroClass.toSMul DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Pi.instZero Pi.topologicalSpace setOf Set.MapsTo DFunLike.coe funLike	—	nhds_induced Filter.HasBasis.comap UniformOnFun.hasBasis_nhds_zero_of_basis isUniformAddGroup_of_addCommGroup Bornology.isVonNBounded_empty directedOn_of_sup_mem Bornology.IsVonNBounded.union
hasSum_eval 📖	mathematical	ContinuousSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing HasSum ContinuousMultilinearMap addCommMonoid IsTopologicalAddGroup.toContinuousAdd instTopologicalSpace SummationFilter.unconditional	DFunLike.coe funLike	—	IsTopologicalAddGroup.toContinuousAdd HasSum.map AddMonoidHom.instAddMonoidHomClass ContinuousEvalConst.continuous_eval_const instContinuousEvalConstForall
instCompleteSpace 📖	mathematical	ContinuousSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing IsTopologicalAddGroup	CompleteSpace ContinuousMultilinearMap instUniformSpace	—	completeSpace Topology.IsCoherentWith.of_seq Bornology.IsVonNBounded.insert instContinuousSMulForall Filter.Tendsto.isVonNBounded_range Pi.topologicalAddGroup
instContinuousConstSMul 📖	mathematical	—	ContinuousConstSMul ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid instTopologicalSpace instSMul DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid	—	UniformContinuousConstSMul.to_continuousConstSMul isUniformAddGroup_of_addCommGroup instUniformContinuousConstSMul
instContinuousEvalConstForall 📖	mathematical	ContinuousSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	ContinuousEvalConst ContinuousMultilinearMap funLike instTopologicalSpace	—	isUniformAddGroup_of_addCommGroup UniformContinuous.continuous uniformContinuous_eval_const
instContinuousSMul 📖	mathematical	—	ContinuousSMul ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction ContinuousSMul.continuousConstSMul UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing instTopologicalSpace	—	IsTopologicalAddGroup.toContinuousAdd ContinuousSMul.continuousConstSMul smulCommClass_self UniformOnFun.continuousSMul_induced_of_image_bounded isUniformAddGroup_of_addCommGroup LinearMap.semilinearMapClass Topology.IsEmbedding.isInducing IsUniformAddGroup.to_topologicalAddGroup isEmbedding_toUniformOnFun Bornology.IsVonNBounded.image_multilinear
instIsTopologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid instTopologicalSpace AddCommGroup.toAddGroup instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing	—	IsUniformAddGroup.to_topologicalAddGroup isUniformAddGroup_of_addCommGroup instIsUniformAddGroup
instIsUniformAddGroup 📖	mathematical	—	IsUniformAddGroup ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace instUniformSpace AddCommGroup.toAddGroup instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing IsUniformAddGroup.to_topologicalAddGroup	—	IsUniformAddGroup.to_topologicalAddGroup IsUniformInducing.isUniformAddGroup instIsUniformAddGroupUniformOnFun AddMonoidHom.instAddMonoidHomClass IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_toUniformOnFun
instT2Space 📖	mathematical	ContinuousSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	T2Space ContinuousMultilinearMap instTopologicalSpace	—	T2Space.of_injective_continuous Pi.t2Space DFunLike.coe_injective continuous_coeFun instContinuousEvalConstForall
instT3Space 📖	mathematical	ContinuousSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	T3Space ContinuousMultilinearMap instTopologicalSpace	—	instT3Space T1Space.t0Space T2Space.t1Space instT2Space IsTopologicalAddGroup.regularSpace instIsTopologicalAddGroup
instUniformContinuousConstSMul 📖	mathematical	—	UniformContinuousConstSMul ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace instUniformSpace instSMul DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid	—	IsUniformInducing.uniformContinuousConstSMul UniformFunOn.uniformContinuousConstSMul uniformContinuousConstSMul_of_continuousConstSMul IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_toUniformOnFun
isEmbedding_restrictScalars 📖	mathematical	ContinuousSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing IsScalarTower Algebra.toSMul Semifield.toCommSemiring NontriviallyNormedField.toNormedField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra	Topology.IsEmbedding ContinuousMultilinearMap instTopologicalSpace restrictScalars	—	IsUniformEmbedding.isEmbedding isUniformAddGroup_of_addCommGroup isUniformEmbedding_restrictScalars
isEmbedding_toUniformOnFun 📖	mathematical	—	Topology.IsEmbedding ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace UniformOnFun setOf Set Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Pi.instSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Pi.instZero Pi.topologicalSpace instTopologicalSpace IsUniformAddGroup.to_topologicalAddGroup UniformOnFun.topologicalSpace toUniformOnFun	—	IsUniformEmbedding.isEmbedding isUniformEmbedding_toUniformOnFun
isUniformEmbedding_restrictScalars 📖	mathematical	IsScalarTower Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid ContinuousSMul UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace	IsUniformEmbedding ContinuousMultilinearMap instUniformSpace restrictScalars	—	IsUniformEmbedding.of_comp_iff isUniformEmbedding_toUniformOnFun Bornology.IsVonNBounded.extend_scalars NontriviallyNormedField.non_trivial norm_algebraMap' NormedDivisionRing.to_normOneClass instContinuousSMulForall Pi.isScalarTower Bornology.IsVonNBounded.restrict_scalars
isUniformEmbedding_toUniformOnFun 📖	mathematical	—	IsUniformEmbedding ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace UniformOnFun setOf Set Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Pi.instSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Pi.instZero Pi.topologicalSpace instUniformSpace UniformOnFun.uniformSpace toUniformOnFun	—	isUniformInducing_toUniformOnFun DFunLike.coe_injective
isUniformInducing_postcomp 📖	mathematical	IsUniformInducing DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike	ContinuousMultilinearMap instUniformSpace ContinuousLinearMap.compContinuousMultilinearMap	—	IsUniformInducing.of_comp_iff isUniformInducing_toUniformOnFun IsUniformInducing.comp UniformOnFun.postcomp_isUniformInducing
isUniformInducing_toUniformOnFun 📖	mathematical	—	IsUniformInducing ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace UniformOnFun setOf Set Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Pi.instSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Pi.instZero Pi.topologicalSpace instUniformSpace UniformOnFun.uniformSpace toUniformOnFun	—	—
range_toUniformOnFun 📖	mathematical	—	Set.range UniformOnFun setOf Set Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Pi.instSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Pi.instZero Pi.topologicalSpace ContinuousMultilinearMap toUniformOnFun Continuous DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.toFun	—	Set.ext cont map_update_add map_update_smul Lean.Meta.FastSubsingleton.elim Lean.Meta.instFastSubsingletonForall Lean.Meta.instFastSubsingletonDecidable
restrictScalarsLinear_apply 📖	mathematical	ContinuousSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing IsScalarTower Algebra.toSMul Semifield.toCommSemiring NontriviallyNormedField.toNormedField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap instTopologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd instModule IsScalarTower.to_smulCommClass' smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid CommRing.toRing ContinuousLinearMap.funLike restrictScalarsLinear restrictScalars	—	IsTopologicalAddGroup.toContinuousAdd IsScalarTower.to_smulCommClass' smulCommClass_self
toUniformOnFun_toFun 📖	mathematical	—	DFunLike.coe Equiv UniformOnFun setOf Set Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Pi.instSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Pi.instZero Pi.topologicalSpace EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.toFun toUniformOnFun ContinuousMultilinearMap funLike	—	—
tsum_eval 📖	mathematical	ContinuousSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Summable ContinuousMultilinearMap addCommMonoid IsTopologicalAddGroup.toContinuousAdd instTopologicalSpace SummationFilter.unconditional	DFunLike.coe funLike tsum	—	IsTopologicalAddGroup.toContinuousAdd HasSum.tsum_eq SummationFilter.instNeBotUnconditional hasSum_eval Summable.hasSum
uniformContinuous_coe_fun 📖	mathematical	ContinuousSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	UniformContinuous ContinuousMultilinearMap instUniformSpace Pi.uniformSpace DFunLike.coe funLike	—	UniformContinuous.comp UniformOnFun.uniformContinuous_toFun Bornology.sUnion_isVonNBounded_eq_univ instContinuousSMulForall IsUniformInducing.uniformContinuous IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_toUniformOnFun
uniformContinuous_eval_const 📖	mathematical	ContinuousSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	UniformContinuous ContinuousMultilinearMap instUniformSpace DFunLike.coe funLike	—	uniformContinuous_pi uniformContinuous_coe_fun
uniformContinuous_restrictScalars 📖	mathematical	IsScalarTower Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid ContinuousSMul UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace	UniformContinuous ContinuousMultilinearMap instUniformSpace restrictScalars	—	IsUniformInducing.uniformContinuous IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_restrictScalars

---

← Back to Index