Topology

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

Statistics

Metric	Count
Definitions continuousMultilinearMapCongrLeft, continuousMultilinearMapCongrRight, compContinuousMultilinearMapL, apply, compContinuousLinearMapL, instTopologicalSpace, instUniformSpace, restrictScalarsLinear, toUniformOnFun	9
Theorems continuousMultilinearMapCongrLeft_apply, continuousMultilinearMapCongrLeft_symm, continuousMultilinearMapCongrRight_apply, continuousMultilinearMapCongrRight_symm, compContinuousMultilinearMapL_apply, apply_apply, compContinuousLinearMapL_apply, completeSpace, continuous_restrictScalars, eventually_nhds_zero_mapsTo, 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, isVonNBounded_image2_apply, range_toUniformOnFun, restrictScalarsLinear_apply, toUniformOnFun_toFun, tsum_eval, uniformContinuous_coe_fun, uniformContinuous_eval_const, uniformContinuous_restrictScalars	36
Total	45

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
continuousMultilinearMapCongrLeft 📖	CompOp	2 math math: continuousMultilinearMapCongrLeft_apply, continuousMultilinearMapCongrLeft_symm
continuousMultilinearMapCongrRight 📖	CompOp	2 math math: continuousMultilinearMapCongrRight_symm, continuousMultilinearMapCongrRight_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousMultilinearMapCongrLeft_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap AddCommGroup.toAddCommMonoid ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousMultilinearMap.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing EquivLike.toFunLike equivLike continuousMultilinearMapCongrLeft ContinuousMultilinearMap.compContinuousLinearMap toContinuousLinearMap	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
continuousMultilinearMapCongrLeft_symm 📖	mathematical	—	symm DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap AddCommGroup.toAddCommMonoid ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousMultilinearMap.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing continuousMultilinearMapCongrLeft	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
continuousMultilinearMapCongrRight_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap AddCommGroup.toAddCommMonoid ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousMultilinearMap.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing EquivLike.toFunLike equivLike continuousMultilinearMapCongrRight ContinuousLinearMap.compContinuousMultilinearMap toContinuousLinearMap	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
continuousMultilinearMapCongrRight_symm 📖	mathematical	—	symm DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap AddCommGroup.toAddCommMonoid ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousMultilinearMap.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing continuousMultilinearMapCongrRight	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self

ContinuousLinearMap

Definitions

Name	Category	Theorems
compContinuousMultilinearMapL 📖	CompOp	1 math math: compContinuousMultilinearMapL_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compContinuousMultilinearMapL_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap AddCommGroup.toAddCommMonoid ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousMultilinearMap.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing funLike topologicalSpace addCommMonoid ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing ContinuousMultilinearMap.instIsTopologicalAddGroup module ContinuousMultilinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousMultilinearMap.instContinuousConstSMul compContinuousMultilinearMapL compContinuousMultilinearMap	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self ContinuousMultilinearMap.instIsTopologicalAddGroup ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul

ContinuousMultilinearMap

Definitions

Name	Category	Theorems
apply 📖	CompOp	5 math math: HasFDerivWithinAt.continuousMultilinearMap_apply, apply_apply, HasStrictFDerivAt.continuousMultilinearMap_apply, hasStrictFDerivAt_uncurry, HasFDerivAt.continuousMultilinearMap_apply
compContinuousLinearMapL 📖	CompOp	8 math math: HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap, HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap, fderivWithin_continuousMultilinearMapCompContinuousLinearMap, fderiv_continuousMultilinearMapCompContinuousLinearMap, hasStrictFDerivAt_compContinuousLinearMap, HasStrictFDerivAt.continuousMultilinearMapCompContinuousLinearMap, compContinuousLinearMapL_apply, norm_compContinuousLinearMapL_le
instTopologicalSpace 📖	CompOp	167 math math: fderiv_iteratedFDeriv, HasFDerivWithinAt.continuousMultilinearMap_apply, 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, eventually_nhds_zero_mapsTo, FormalMultilinearSeries.changeOriginSeries_summable_aux₃, HasFDerivWithinAt.linear_multilinear_comp, iteratedFDerivWithin_succ_eq_comp_left, contDiffOn_iff_continuousOn_differentiableOn, HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap, PiTensorProduct.toDualContinuousMultilinearMap_apply_apply, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_apply_le, norm_smulRightL_le, HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap, ContinuousLinearMap.cpolynomialOn_uncurry_of_multilinear, VectorFourier.fourierPowSMulRight_eq_comp, HasFTaylorSeriesUpTo.fderiv_eq, 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, ContinuousLinearMap.compContinuousMultilinearMapL_apply, ContDiffOn.continuousOn_iteratedFDerivWithin, HasFTaylorSeriesUpToOn.cont, restrictScalarsLinear_apply, contDiffOn_nat_iff_continuousOn_differentiableOn, fderivWithin_continuousMultilinear_apply_const_apply, ContDiff.differentiable_iteratedFDeriv, ContinuousLinearMap.analyticWithinAt_uncurry_of_multilinear, FormalMultilinearSeries.iteratedFDerivSeries_eq_zero, hasBasis_nhds_zero, fderivWithin_continuousMultilinear_apply_const, FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm_apply_le, hasFTaylorSeriesUpToOn_top_iff', iteratedFDeriv_tsum, contDiff_iff_continuous_differentiable, hasFTaylorSeriesUpToOn_succ_iff_right, ContinuousLinearMap.coe_flipMultilinearEquiv, FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum, DifferentiableAt.continuousMultilinearMapCompContinuousLinearMap, 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, Differentiable.continuousMultilinearMapCompContinuousLinearMap, hasFTaylorSeriesUpToOn_succ_nat_iff_right, tsum_eval, 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, fderivWithin_continuousMultilinearMapCompContinuousLinearMap, MultilinearMap.mkContinuousLinear_norm_le', norm_fderivWithin_iteratedFDerivWithin, ContinuousLinearEquiv.continuousMultilinearMapCongrRight_symm, ContinuousAlternatingMap.toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap, ContinuousLinearMap.norm_uncurryMid, ContinuousLinearMap.uncurryLeft_norm, MeasureTheory.AEStronglyMeasurable.fourierPowSMulRight, fderiv_continuousMultilinear_apply_const_apply, ContDiff.continuous_iteratedFDeriv', ContinuousLinearMap.continuous_uncurry_of_multilinear, ContDiffMapSupportedIn.isUniformEmbedding_pi_structureMapCLM, isEmbedding_toUniformOnFun, MultilinearMap.mkContinuousMultilinear_norm_le', curryFinFinset_symm_apply_piecewise_const, DifferentiableOn.continuousMultilinearMapCompContinuousLinearMap, 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, fderiv_continuousMultilinearMapCompContinuousLinearMap, contDiff_nat_iff_continuous_differentiable, MultilinearMap.mkContinuousMultilinear_norm_le, hasStrictFDerivAt_compContinuousLinearMap, fderiv_continuousMultilinear_apply_const, curryMid_apply, PiTensorProduct.toDualContinuousMultilinearMap_le_projectiveSeminorm, ContinuousLinearMap.hasFDerivAt_uncurry_of_multilinear, instT2Space, HasFDerivAt.linear_multilinear_comp, HasStrictFDerivAt.continuousMultilinearMapCompContinuousLinearMap, 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, ContinuousAlternatingMap.liftCLM_apply, 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, HasStrictFDerivAt.continuousMultilinearMap_apply, instIsTopologicalAddGroup, curryFinFinset_apply, FormalMultilinearSeries.changeOriginSeriesTerm_bound, ContinuousLinearMap.norm_map_removeNth_le, hasStrictFDerivAt_uncurry, compContinuousLinearMapContinuousMultilinear_apply_apply, fderivWithin_restrictScalars_comp, norm_curryMid, continuous_restrictScalars, PiTensorProduct.injectiveSeminorm_def, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_le, DifferentiableWithinAt.continuousMultilinearMapCompContinuousLinearMap, ContinuousLinearMap.continuousAt_uncurry_of_multilinear, curryMidEquiv_symm_apply, iteratedFDeriv_succ_apply_left, HasFDerivAt.continuousMultilinearMap_apply
instUniformSpace 📖	CompOp	15 math math: ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMap, uniformContinuous_eval_const, uniformity_eq_seminorm, 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap AddCommGroup.toAddCommMonoid instTopologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing ContinuousLinearMap.funLike apply funLike	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
compContinuousLinearMapL_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap AddCommGroup.toAddCommMonoid instTopologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing ContinuousLinearMap.funLike compContinuousLinearMapL compContinuousLinearMap	—	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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace 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 UniformSpace.to_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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid NontriviallyNormedField.toNormedField instTopologicalSpace restrictScalars Algebra.toSMul Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra	—	Topology.IsEmbedding.continuous isEmbedding_restrictScalars
eventually_nhds_zero_mapsTo 📖	mathematical	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 Set Filter Filter.instMembership nhds	Filter.Eventually ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid Set.MapsTo DFunLike.coe funLike nhds instTopologicalSpace instZero	—	Filter.HasBasis.mem_of_mem hasBasis_nhds_zero
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	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 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	HasSum AddCommGroup.toAddCommMonoid DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField funLike SummationFilter.unconditional	—	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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace 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 SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid 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 SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Module.toDistribMulAction ContinuousSMul.continuousConstSMul UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid 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 SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid NontriviallyNormedField.toNormedField instTopologicalSpace restrictScalars Algebra.toSMul Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra	—	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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace NontriviallyNormedField.toNormedField instUniformSpace restrictScalars Algebra.toSMul Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra	—	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	IsUniformInducing ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace 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	—	—
isVonNBounded_image2_apply 📖	mathematical	Bornology.IsVonNBounded ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing instZero instTopologicalSpace Pi.instSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass Pi.instZero Pi.topologicalSpace	Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing 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 NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set.image2 ContinuousMultilinearMap DFunLike.coe funLike	—	smulCommClass_self Filter.mp_mem eventually_nhds_zero_mapsTo Filter.univ_mem' Set.image2_subset_iff Set.smul_mem_smul_set
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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap AddCommGroup.toAddCommMonoid instTopologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instModule IsScalarTower.to_smulCommClass' Semifield.toCommSemiring NormedAlgebra.toAlgebra SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing ContinuousLinearMap.funLike restrictScalarsLinear restrictScalars Algebra.toSMul SeminormedRing.toRing	—	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 ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike tsum addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instTopologicalSpace SummationFilter.unconditional	—	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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace NontriviallyNormedField.toNormedField instUniformSpace restrictScalars Algebra.toSMul Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra	—	IsUniformInducing.uniformContinuous IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_restrictScalars

---

← Back to Index