Commit 2023-04-17 14:43 1d84d7df

View on Github →

feat: port Analysis.NormedSpace.Pointwise (#3479)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/Pointwise.lean

added theorem Metric.Bounded.smul

added theorem NormedSpace.sphere_nonempty

added theorem affinity_unitBall

added theorem affinity_unitClosedBall

added theorem ball_add_ball

added theorem ball_add_closedBall

added theorem ball_sub_ball

added theorem ball_sub_closedBall

added theorem closedBall_add_ball

added theorem closedBall_add_closedBall

added theorem closedBall_sub_ball

added theorem closedBall_sub_closedBall

added theorem closure_thickening

added theorem cthickening_ball

added theorem cthickening_closedBall

added theorem cthickening_cthickening

added theorem cthickening_thickening

added theorem disjoint_ball_ball_iff

added theorem disjoint_ball_closedBall_iff

added theorem disjoint_closedBall_ball_iff

added theorem disjoint_closedBall_closedBall_iff

added theorem eventually_singleton_add_smul_subset

added theorem exists_dist_eq

added theorem exists_dist_le_le

added theorem exists_dist_le_lt

added theorem exists_dist_lt_le

added theorem exists_dist_lt_lt

added theorem infEdist_cthickening

added theorem infEdist_thickening

added theorem smul_ball

added theorem smul_closedBall'

added theorem smul_closedBall

added theorem smul_closedUnitBall

added theorem smul_closedUnitBall_of_nonneg

added theorem smul_sphere'

added theorem smul_sphere

added theorem smul_unitBall

added theorem smul_unitBall_of_pos

added theorem thickening_ball

added theorem thickening_closedBall

added theorem thickening_cthickening

added theorem thickening_thickening