Topology

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

Statistics

Metric	Count
Definitions apply, compContinuousLinearMapCLM, instTopologicalSpace, instUniformSpace, liftCLM, restrictScalarsCLM, toContinuousMultilinearMapCLM, continuousAlternatingMapCongr, continuousAlternatingMapCongrLeft, continuousAlternatingMapCongrRight, compContinuousAlternatingMapCLM	11
Theorems apply_apply, compContinuousLinearMapCLM_apply, completeSpace, continuous_restrictScalars, continuous_toContinuousMultilinearMap, hasBasis_nhds_zero, hasBasis_nhds_zero_of_basis, hasSum_eval, instCompleteSpace, instContinuousConstSMul, instContinuousEvalConst, instContinuousSMul, instIsTopologicalAddGroup, instIsUniformAddGroup, instT2Space, instT3Space, instUniformContinuousConstSMul, isClosedEmbedding_toContinuousMultilinearMap, isClosed_range_toContinuousMultilinearMap, isEmbedding_restrictScalars, isEmbedding_toContinuousMultilinearMap, isUniformEmbedding_restrictScalars, isUniformEmbedding_toContinuousMultilinearMap, isUniformInducing_postcomp, liftCLM_apply, restrictScalarsCLM_apply, toContinuousMultilinearMapCLM_apply, tsum_eval, uniformContinuous_coe_fun, uniformContinuous_eval_const, uniformContinuous_restrictScalars, uniformContinuous_toContinuousMultilinearMap, continuousAlternatingMapCongrLeft_apply, continuousAlternatingMapCongrRight_apply, continuousAlternatingMapCongrRight_symm, continuousAlternatingMapCongr_apply, compContinuousAlternatingMapCLM_apply_apply	37
Total	48

ContinuousAlternatingMap

Definitions

Name	Category	Theorems
apply 📖	CompOp	6 math math: HasFDerivWithinAt.continuousAlternatingMap_apply, fderiv_continuousAlternatingMap_apply, HasFDerivAt.continuousAlternatingMap_apply, apply_apply, HasStrictFDerivAt.continuousAlternatingMap_apply, fderivWithin_continuousAlternatingMap_apply
compContinuousLinearMapCLM 📖	CompOp	9 math math: hasStrictFDerivAt_compContinuousLinearMap, fderiv_continuousAlternatingMapCompContinuousLinearMap, continuous_compContinuousLinearMapCLM, fderivWithin_continuousAlternatingMapCompContinuousLinearMap, HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap, fderivCompContinuousLinearMap_eq_alternatizeUncurryFin, HasStrictFDerivAt.continuousAlternatingMapCompContinuousLinearMap, HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap, compContinuousLinearMapCLM_apply
instTopologicalSpace 📖	CompOp	79 math math: isEmbedding_restrictScalars, isClosedEmbedding_toContinuousMultilinearMap, hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff, hasStrictFDerivAt_compContinuousLinearMap, tsum_eval, fderiv_continuousAlternatingMap_apply_const, DifferentiableAt.continuousAlternatingMapCompContinuousLinearMap, curryLeft_smul, HasFDerivWithinAt.continuousAlternatingMap_apply, toAlternatingMap_curryLeft, fderiv_continuousAlternatingMapCompContinuousLinearMap, instContinuousSMul, fderiv_continuousAlternatingMap_apply, instContinuousConstSMul, HasFDerivAt.continuousAlternatingMap_apply, curryLeft_apply_apply, isEmbedding_toContinuousMultilinearMap, fderivWithin_continuousAlternatingMap_apply_const_apply, alternatizeUncurryFin_smul, alternatizeUncurryFin_constOfIsEmptyLIE_comp, alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply, continuous_compContinuousLinearMapCLM, instIsTopologicalAddGroup, DifferentiableWithinAt.continuousAlternatingMapCompContinuousLinearMap, norm_curryLeft, apply_apply, fderivWithin_continuousAlternatingMapCompContinuousLinearMap, norm_alternatizeUncurryFinCLM_le, AlternatingMap.mkContinuousAlternating_norm_le, curryLeft_compContinuousAlternatingMap, HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap, fderivCompContinuousLinearMap_eq_alternatizeUncurryFin, curryLeft_compContinuousLinearMap, ContinuousLinearEquiv.continuousAlternatingMapCongrRight_symm, toContinuousMultilinearMapCLM_apply, fderivCompContinuousLinearMapCLM_apply, toAlternatingMap_alternatizeUncurryFin, hasBasis_nhds_zero, toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap, continuous_restrictScalars, HasStrictFDerivAt.continuousAlternatingMap_apply, instT3Space, curryLeft_same, curryLeft_zero, toContinuousMultilinearMap_curryLeft, fderiv_continuousAlternatingMap_apply_apply, restrictScalarsCLM_apply, fderivWithin_continuousAlternatingMap_apply_apply, ContinuousLinearEquiv.continuousAlternatingMapCongrLeft_apply, hasBasis_nhds_zero_of_basis, ContinuousLinearEquiv.continuousAlternatingMapCongrRight_apply, alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetric, fderivWithin_continuousAlternatingMap_apply_const, fderivCompContinuousLinearMap_apply, curryLeft_add, AlternatingMap.mkContinuousLinear_norm_le, curryLeftLI_apply, fderivCompContinuousLinearMap_of_isEmpty, norm_alternatizeUncurryFin_le, AlternatingMap.mkContinuousAlternating_norm_le_max, ContinuousLinearEquiv.continuousAlternatingMapCongr_apply, alternatizeUncurryFin_add, instT2Space, fderivWithin_continuousAlternatingMap_apply, ContinuousLinearMap.compContinuousAlternatingMapCLM_apply_apply, liftCLM_apply, instContinuousEval, HasStrictFDerivAt.continuousAlternatingMapCompContinuousLinearMap, AlternatingMap.mkContinuousLinear_norm_le_max, fderiv_continuousAlternatingMap_apply_const_apply, HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap, continuous_toContinuousMultilinearMap, alternatizeUncurryFin_fderivCompContinuousLinearMap_eq_zero, compContinuousLinearMapCLM_apply, AlternatingMap.mkContinuousAlternating_apply, alternatizeUncurryFin_apply, instContinuousEvalConst, alternatizeUncurryFinCLM_apply, ContinuousLinearMap.flipAlternating_apply_apply
instUniformSpace 📖	CompOp	11 math math: uniformContinuous_eval_const, isUniformEmbedding_toContinuousMultilinearMap, instIsUniformAddGroup, isUniformInducing_postcomp, isUniformEmbedding_restrictScalars, instUniformContinuousConstSMul, uniformContinuous_coe_fun, completeSpace, uniformContinuous_toContinuousMultilinearMap, instCompleteSpace, uniformContinuous_restrictScalars
liftCLM 📖	CompOp	1 math math: liftCLM_apply
restrictScalarsCLM 📖	CompOp	1 math math: restrictScalarsCLM_apply
toContinuousMultilinearMapCLM 📖	CompOp	3 math math: hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff, toContinuousMultilinearMapCLM_apply, toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ContinuousAlternatingMap 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
compContinuousLinearMapCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ContinuousAlternatingMap 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 compContinuousLinearMapCLM compContinuousLinearMap CommSemiring.toSemiring Semifield.toCommSemiring	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
completeSpace 📖	mathematical	Topology.IsCoherentWith Pi.topologicalSpace setOf Set Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Function.hasSMul 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 Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	CompleteSpace ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace instUniformSpace	—	ContinuousMultilinearMap.completeSpace completeSpace_iff_isComplete_range IsUniformEmbedding.isUniformInducing isUniformEmbedding_toContinuousMultilinearMap IsClosed.isComplete isClosed_range_toContinuousMultilinearMap IsUniformAddGroup.to_topologicalAddGroup SeparationQuotient.instIsUniformAddGroup IsUniformInducing.completeSpace_congr isUniformInducing_postcomp IsTopologicalAddGroup.toContinuousAdd ext SeparationQuotient.mk_outCLM SeparationQuotient.instContinuousConstSMul SeparationQuotient.instCompleteSpace SeparationQuotient.t2Space instR1Space UniformSpace.to_regularSpace
continuous_restrictScalars 📖	mathematical	—	Continuous ContinuousAlternatingMap 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
continuous_toContinuousMultilinearMap 📖	mathematical	—	Continuous ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid ContinuousMultilinearMap instTopologicalSpace ContinuousMultilinearMap.instTopologicalSpace toContinuousMultilinearMap	—	Topology.IsEmbedding.continuous isEmbedding_toContinuousMultilinearMap
hasBasis_nhds_zero 📖	mathematical	—	Filter.HasBasis ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid Set nhds instTopologicalSpace instZero Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid 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 ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid Set nhds instTopologicalSpace instZero Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Pi.topologicalSpace setOf Set.MapsTo DFunLike.coe funLike	—	nhds_induced Filter.HasBasis.comap ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis
hasSum_eval 📖	mathematical	HasSum ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instTopologicalSpace SummationFilter.unconditional	HasSum AddCommGroup.toAddCommMonoid DFunLike.coe ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField funLike SummationFilter.unconditional	—	IsTopologicalAddGroup.toContinuousAdd HasSum.map AddMonoidHom.instAddMonoidHomClass ContinuousEvalConst.continuous_eval_const instContinuousEvalConst
instCompleteSpace 📖	mathematical	—	CompleteSpace ContinuousAlternatingMap 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 ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid instTopologicalSpace instSMul	—	Topology.IsInducing.continuousConstSMul ContinuousMultilinearMap.instContinuousConstSMul Topology.IsEmbedding.toIsInducing isEmbedding_toContinuousMultilinearMap
instContinuousEvalConst 📖	mathematical	—	ContinuousEvalConst ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike instTopologicalSpace	—	ContinuousEvalConst.of_continuous_forget ContinuousMultilinearMap.instContinuousEvalConstForall continuous_toContinuousMultilinearMap
instContinuousSMul 📖	mathematical	—	ContinuousSMul ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid instSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 DistribMulAction.toDistribSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing instTopologicalSpace	—	Topology.IsInducing.continuousSMul ContinuousSMul.continuousConstSMul smulCommClass_self ContinuousMultilinearMap.instContinuousSMul Topology.IsEmbedding.toIsInducing isEmbedding_toContinuousMultilinearMap continuous_id
instIsTopologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid instTopologicalSpace AddCommGroup.toAddGroup instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing	—	Topology.IsInducing.topologicalAddGroup ContinuousMultilinearMap.instIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd AddMonoid.continuousConstSMul_nat AddMonoid.nat_smulCommClass' DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Topology.IsEmbedding.toIsInducing isEmbedding_toContinuousMultilinearMap
instIsUniformAddGroup 📖	mathematical	—	IsUniformAddGroup ContinuousAlternatingMap 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	—	IsUniformInducing.isUniformAddGroup IsTopologicalAddGroup.toContinuousAdd IsUniformAddGroup.to_topologicalAddGroup AddMonoid.continuousConstSMul_nat AddMonoid.nat_smulCommClass' ContinuousMultilinearMap.instIsUniformAddGroup DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_toContinuousMultilinearMap
instT2Space 📖	mathematical	—	T2Space ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid instTopologicalSpace	—	T2Space.of_injective_continuous Pi.t2Space DFunLike.coe_injective continuous_coeFun instContinuousEvalConst
instT3Space 📖	mathematical	—	T3Space ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid instTopologicalSpace	—	instT3Space T1Space.t0Space T2Space.t1Space instT2Space IsTopologicalAddGroup.regularSpace instIsTopologicalAddGroup
instUniformContinuousConstSMul 📖	mathematical	—	UniformContinuousConstSMul ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace instUniformSpace instSMul	—	IsUniformInducing.uniformContinuousConstSMul ContinuousMultilinearMap.instUniformContinuousConstSMul IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_toContinuousMultilinearMap
isClosedEmbedding_toContinuousMultilinearMap 📖	mathematical	—	Topology.IsClosedEmbedding ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid ContinuousMultilinearMap instTopologicalSpace ContinuousMultilinearMap.instTopologicalSpace toContinuousMultilinearMap	—	isEmbedding_toContinuousMultilinearMap isClosed_range_toContinuousMultilinearMap
isClosed_range_toContinuousMultilinearMap 📖	mathematical	—	IsClosed ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid ContinuousMultilinearMap.instTopologicalSpace Set.range ContinuousAlternatingMap toContinuousMultilinearMap	—	range_toContinuousMultilinearMap Set.setOf_forall Set.iInter_congr_Prop isClosed_iInter IsClosed.preimage ContinuousEvalConst.continuous_eval_const ContinuousMultilinearMap.instContinuousEvalConstForall isClosed_singleton T2Space.t1Space
isEmbedding_restrictScalars 📖	mathematical	—	Topology.IsEmbedding ContinuousAlternatingMap 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_toContinuousMultilinearMap 📖	mathematical	—	Topology.IsEmbedding ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid ContinuousMultilinearMap instTopologicalSpace ContinuousMultilinearMap.instTopologicalSpace toContinuousMultilinearMap	—	IsUniformEmbedding.isEmbedding isUniformAddGroup_of_addCommGroup isUniformEmbedding_toContinuousMultilinearMap
isUniformEmbedding_restrictScalars 📖	mathematical	—	IsUniformEmbedding ContinuousAlternatingMap 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_toContinuousMultilinearMap IsUniformEmbedding.comp ContinuousMultilinearMap.isUniformEmbedding_restrictScalars
isUniformEmbedding_toContinuousMultilinearMap 📖	mathematical	—	IsUniformEmbedding ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace ContinuousMultilinearMap instUniformSpace ContinuousMultilinearMap.instUniformSpace toContinuousMultilinearMap	—	toContinuousMultilinearMap_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 ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace instUniformSpace ContinuousLinearMap.compContinuousAlternatingMap	—	IsUniformInducing.of_comp_iff IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_toContinuousMultilinearMap IsUniformInducing.comp ContinuousMultilinearMap.isUniformInducing_postcomp
liftCLM_apply 📖	mathematical	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid ContinuousMultilinearMap.funLike ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring 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 ContinuousLinearMap.funLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	DFunLike.coe ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring 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 liftCLM ContinuousMultilinearMap ContinuousMultilinearMap.funLike ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.addCommMonoid ContinuousMultilinearMap.instModule	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
restrictScalarsCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ContinuousAlternatingMap 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 restrictScalarsCLM restrictScalars Algebra.toSMul SeminormedRing.toRing	—	IsTopologicalAddGroup.toContinuousAdd IsScalarTower.to_smulCommClass' smulCommClass_self
toContinuousMultilinearMapCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid instTopologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousMultilinearMap ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.addCommMonoid instModule ContinuousMultilinearMap.instModule ContinuousLinearMap.funLike toContinuousMultilinearMapCLM toContinuousMultilinearMap	—	IsTopologicalAddGroup.toContinuousAdd
tsum_eval 📖	mathematical	Summable ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instTopologicalSpace SummationFilter.unconditional	DFunLike.coe ContinuousAlternatingMap 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	—	UniformContinuous ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace instUniformSpace Pi.uniformSpace DFunLike.coe funLike	—	UniformContinuous.comp ContinuousMultilinearMap.uniformContinuous_coe_fun uniformContinuous_toContinuousMultilinearMap
uniformContinuous_eval_const 📖	mathematical	—	UniformContinuous ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace instUniformSpace DFunLike.coe funLike	—	uniformContinuous_pi uniformContinuous_coe_fun
uniformContinuous_restrictScalars 📖	mathematical	—	UniformContinuous ContinuousAlternatingMap 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
uniformContinuous_toContinuousMultilinearMap 📖	mathematical	—	UniformContinuous ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace ContinuousMultilinearMap instUniformSpace ContinuousMultilinearMap.instUniformSpace toContinuousMultilinearMap	—	IsUniformInducing.uniformContinuous IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_toContinuousMultilinearMap

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
continuousAlternatingMapCongr 📖	CompOp	1 math math: continuousAlternatingMapCongr_apply
continuousAlternatingMapCongrLeft 📖	CompOp	1 math math: continuousAlternatingMapCongrLeft_apply
continuousAlternatingMapCongrRight 📖	CompOp	2 math math: continuousAlternatingMapCongrRight_symm, continuousAlternatingMapCongrRight_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousAlternatingMapCongrLeft_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousAlternatingMap AddCommGroup.toAddCommMonoid ContinuousAlternatingMap.instTopologicalSpace ContinuousAlternatingMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousAlternatingMap.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing EquivLike.toFunLike equivLike continuousAlternatingMapCongrLeft ContinuousAlternatingMap.compContinuousLinearMap toContinuousLinearMap symm	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
continuousAlternatingMapCongrRight_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousAlternatingMap AddCommGroup.toAddCommMonoid ContinuousAlternatingMap.instTopologicalSpace ContinuousAlternatingMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousAlternatingMap.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing EquivLike.toFunLike equivLike continuousAlternatingMapCongrRight ContinuousLinearMap.compContinuousAlternatingMap toContinuousLinearMap	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
continuousAlternatingMapCongrRight_symm 📖	mathematical	—	symm DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousAlternatingMap AddCommGroup.toAddCommMonoid ContinuousAlternatingMap.instTopologicalSpace ContinuousAlternatingMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousAlternatingMap.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing continuousAlternatingMapCongrRight	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
continuousAlternatingMapCongr_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousAlternatingMap AddCommGroup.toAddCommMonoid ContinuousAlternatingMap.instTopologicalSpace ContinuousAlternatingMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousAlternatingMap.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing EquivLike.toFunLike equivLike continuousAlternatingMapCongr ContinuousLinearMap.compContinuousAlternatingMap toContinuousLinearMap ContinuousAlternatingMap.compContinuousLinearMap symm	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self

ContinuousLinearMap

Definitions

Name	Category	Theorems
compContinuousAlternatingMapCLM 📖	CompOp	1 math math: compContinuousAlternatingMapCLM_apply_apply

Theorems

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

---

← Back to Index