Commit 2022-01-14 17:47 653fe45e

View on Github →

feat(analysis/seminorm): semilattice_sup on seminorms and lemmas about ball (#11329) Define bot and the the binary sup on seminorms, and some lemmas about the supremum of a finite number of seminorms. Shows that the unit ball of the supremum is given by the intersection of the unit balls.

Estimated changes

Modified src/analysis/seminorm.lean

added theorem seminorm.ball_bot

added theorem seminorm.ball_finset_sup'

added theorem seminorm.ball_finset_sup

added theorem seminorm.ball_finset_sup_eq_Inter

added theorem seminorm.ball_sup

added theorem seminorm.ball_zero'

added theorem seminorm.bot_eq_zero

added theorem seminorm.coe_bot

added theorem seminorm.coe_sup

added theorem seminorm.coe_zero

modified theorem seminorm.ext

added theorem seminorm.finset_sup_apply

added theorem seminorm.le_def

added theorem seminorm.lt_def