Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-09 00:39 e71a12cd

View on Github →

feat(analysis/seminorm): closed balls for a seminorm (#16676) This introduces the closed ball version of seminorm.ball and duplicates a bunch of API. My motivation is the general Banach-Steinhaus theorem in barreled space (one characterization of barrels is that they are exactly closed unit balls of lower semicontinuous seminorms), and I didn't see any reason not do go full duplication here.

Estimated changes

Modified src/analysis/seminorm.lean

added theorem seminorm.balanced_closed_ball_zero

added theorem seminorm.ball_subset_closed_ball

added def seminorm.closed_ball

added theorem seminorm.closed_ball_add_closed_ball_subset

added theorem seminorm.closed_ball_antitone

added theorem seminorm.closed_ball_bot

added theorem seminorm.closed_ball_comp

added theorem seminorm.closed_ball_eq_bInter_ball

added theorem seminorm.closed_ball_eq_emptyset

added theorem seminorm.closed_ball_finset_sup'

added theorem seminorm.closed_ball_finset_sup

added theorem seminorm.closed_ball_finset_sup_eq_Inter

added theorem seminorm.closed_ball_mono

added theorem seminorm.closed_ball_smul

added theorem seminorm.closed_ball_smul_closed_ball

added theorem seminorm.closed_ball_sup

added theorem seminorm.closed_ball_zero'

added theorem seminorm.closed_ball_zero_eq

added theorem seminorm.closed_ball_zero_eq_preimage_closed_ball

added theorem seminorm.convex_closed_ball

added theorem seminorm.mem_closed_ball

added theorem seminorm.mem_closed_ball_self

added theorem seminorm.mem_closed_ball_zero

added theorem seminorm.preimage_metric_ball

added theorem seminorm.preimage_metric_closed_ball

Modified src/topology/metric_space/basic.lean

added theorem metric.closed_ball_eq_bInter_ball