Commit 2023-04-12 19:26 844d0f44

View on Github →

feat: port Analysis.NormedSpace.Basic (#3280)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/RestrictScalars.lean

Modified Mathlib/Analysis/Normed/Group/Basic.lean

Created Mathlib/Analysis/NormedSpace/Basic.lean

added theorem Filter.IsBoundedUnder.smul_tendsto_zero

added theorem Filter.Tendsto.zero_smul_isBoundedUnder_le

added def Module.RestrictScalars.normedSpaceOrig

added def NormedAlgebra.induced

added theorem NormedSpace.exists_lt_norm

added def NormedSpace.induced

added def NormedSpace.restrictScalars

added theorem abs_norm_eq_norm

added theorem algebraMap_isometry

added theorem closure_ball

added theorem coe_homeomorphUnitBall_apply_zero

added theorem dist_smul_le

added theorem dist_smul₀

added theorem eventually_nhds_norm_smul_sub_lt

added theorem exists_norm_eq

added theorem frontier_ball

added theorem frontier_closedBall'

added theorem frontier_closedBall

added theorem interior_closedBall'

added theorem interior_closedBall

added theorem inv_norm_smul_mem_closed_unit_ball

added theorem lipschitzWith_smul

added theorem nndist_smul_le

added theorem nndist_smul₀

added theorem nnnorm_algebraMap

added theorem nnnorm_algebraMap_nNReal

added theorem nnnorm_algebra_map'

added theorem nnnorm_smul

added theorem nnnorm_smul_le

added theorem nnnorm_surjective

added theorem norm_algebraMap

added theorem norm_algebraMap_nNReal

added theorem norm_algebra_map'

added theorem norm_smul

added theorem norm_smul_le

added theorem norm_smul_of_nonneg

added theorem norm_zsmul

added theorem range_nnnorm

added theorem range_norm

added theorem rescale_to_shell

added theorem rescale_to_shell_semi_normed

added theorem rescale_to_shell_semi_normed_zpow

added theorem rescale_to_shell_zpow

Modified Mathlib/Tactic/Continuity.lean