Commit 2024-09-08 21:52 7b6e74c1

View on Github →

feat: topology on ContinuousAlternatingMaps (#16374)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Algebra/ConstMulAction.lean

added theorem Inducing.continuousConstSMul

Created Mathlib/Topology/Algebra/Module/Alternating/Topology.lean

added def ContinuousAlternatingMap.apply

added theorem ContinuousAlternatingMap.apply_apply

added theorem ContinuousAlternatingMap.completeSpace

added theorem ContinuousAlternatingMap.continuous_coe_fun

added theorem ContinuousAlternatingMap.continuous_eval_const

added theorem ContinuousAlternatingMap.continuous_restrictScalars

added theorem ContinuousAlternatingMap.continuous_toContinuousMultilinearMap

added theorem ContinuousAlternatingMap.embedding_restrictScalars

added theorem ContinuousAlternatingMap.embedding_toContinuousMultilinearMap

added theorem ContinuousAlternatingMap.hasBasis_nhds_zero

added theorem ContinuousAlternatingMap.hasBasis_nhds_zero_of_basis

added theorem ContinuousAlternatingMap.hasSum_eval

added def ContinuousAlternatingMap.restrictScalarsCLM

added theorem ContinuousAlternatingMap.tsum_eval

added theorem ContinuousAlternatingMap.uniformContinuous_coe_fun

added theorem ContinuousAlternatingMap.uniformContinuous_eval_const

added theorem ContinuousAlternatingMap.uniformContinuous_restrictScalars

added theorem ContinuousAlternatingMap.uniformContinuous_toContinuousMultilinearMap

added theorem ContinuousAlternatingMap.uniformEmbedding_restrictScalars

added theorem ContinuousAlternatingMap.uniformEmbedding_toContinuousMultilinearMap