Commit 2023-05-20 01:06 78acb825

View on Github →

feat: port Analysis.NormedSpace.FiniteDimension (#4123)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/FiniteDimension.lean

added theorem AffineEquiv.coe_toHomeomorphOfFiniteDimensional

added theorem AffineEquiv.coe_toHomeomorphOfFiniteDimensional_symm

added theorem AffineEquiv.continuous_of_finiteDimensional

added def AffineEquiv.toHomeomorphOfFiniteDimensional

added theorem AffineIsometry.coe_toAffineIsometryEquiv

added def AffineIsometry.toAffineIsometryEquiv

added theorem AffineIsometry.toAffineIsometryEquiv_apply

added theorem AffineMap.continuous_of_finiteDimensional

added theorem AffineSubspace.closed_of_finiteDimensional

added theorem Basis.exists_op_nnnorm_le

added theorem Basis.exists_op_norm_le

added theorem Basis.op_nnnorm_le

added theorem Basis.op_norm_le

added def ContinuousLinearEquiv.piRing

added theorem ContinuousLinearMap.continuous_det

added theorem ContinuousLinearMap.exists_right_inverse_of_surjective

added theorem FiniteDimensional.complete

added theorem FiniteDimensional.proper

added theorem HasCompactMulSupport.eq_one_or_finiteDimensional

added theorem IsEquivalent.summable_iff

added theorem IsEquivalent.summable_iff_nat

added theorem LinearEquiv.closedEmbedding_of_injective

added theorem LinearIsometry.coe_toLinearIsometryEquiv

added def LinearIsometry.toLinearIsometryEquiv

added theorem LinearIsometry.toLinearIsometryEquiv_apply

added theorem LinearMap.exists_antilipschitzWith

added theorem LipschitzOnWith.extend_finite_dimension

added theorem Submodule.closed_of_finiteDimensional

added theorem Submodule.complete_of_finiteDimensional

added theorem closedEmbedding_smul_left

added theorem continuousOn_clm_apply

added theorem continuous_clm_apply

added theorem exists_mem_frontier_infDist_compl_eq_dist

added theorem exists_norm_le_le_norm_sub_of_finset

added theorem exists_seq_norm_le_one_le_norm_sub'

added theorem exists_seq_norm_le_one_le_norm_sub

added theorem finiteDimensional_of_isCompact_closedBall

added theorem finiteDimensional_of_isCompact_closed_ball₀

added theorem isClosedMap_smul_left

added theorem isOpen_setOf_linearIndependent

added theorem isOpen_setOf_nat_le_rank

added theorem lipschitzExtensionConstant_pos

added theorem summable_norm_iff

added theorem summable_of_isBigO'

added theorem summable_of_isBigO_nat'

added theorem summable_of_isEquivalent

added theorem summable_of_isEquivalent_nat