Commit 2026-02-09 11:06 6444c725

View on Github →

refactor(Analysis/Normed/Group): split large file (#34802) Split up > 1500 line file Analysis.Normed.Group.Basic as follows:

  • new file Defs.lean for minimal definitions
  • new file Real.lean for material specific to Real, NNReal and ENNReal
  • some continuity statements moved to the existing file Continuity.lean This gets the Basic file down to below 1000 lines; further splittage may be possible of course.

Estimated changes

deleted theorem Continuous.enorm
deleted theorem ContinuousAt.enorm
deleted theorem ContinuousOn.enorm
deleted theorem ContinuousWithinAt.enorm
deleted theorem NNReal.nnnorm_eq_self
deleted theorem Real.enorm_abs
deleted theorem Real.enorm_eq_ofReal
deleted theorem Real.enorm_eq_ofReal_abs
deleted theorem Real.enorm_natCast
deleted theorem Real.enorm_of_nonneg
deleted theorem Real.le_norm_self
deleted theorem Real.nnnorm_abs
deleted theorem Real.nnnorm_natCast
deleted theorem Real.nnnorm_nnratCast
deleted theorem Real.nnnorm_ofNat
deleted theorem Real.nnnorm_of_nonneg
deleted theorem Real.nnnorm_two
deleted theorem Real.norm_eq_abs
deleted theorem Real.norm_natCast
deleted theorem Real.norm_nnratCast
deleted theorem Real.norm_ofNat
deleted theorem Real.norm_of_nonneg
deleted theorem Real.norm_of_nonpos
deleted theorem Real.norm_two
deleted theorem Real.ofReal_le_enorm
deleted theorem coe_le_enorm
deleted theorem coe_lt_enorm
deleted theorem continuous_enorm
deleted theorem enorm_enorm
deleted theorem enorm_eq_nnnorm
deleted theorem enorm_eq_self
deleted theorem enorm_le_coe
deleted theorem enorm_lt_coe
deleted theorem enorm_lt_top
deleted theorem enorm_ne_top
deleted theorem enorm_norm'
deleted theorem nnnorm_norm'
deleted theorem norm_norm'
deleted theorem tendsto_norm_atTop_atTop
deleted theorem toNNReal_enorm
added theorem Continuous.enorm
added theorem ContinuousAt.enorm
added theorem ContinuousOn.enorm
added theorem continuous_enorm
added theorem coe_le_enorm
added theorem coe_lt_enorm
added theorem enorm_eq_nnnorm
added theorem enorm_le_coe
added theorem enorm_lt_coe
added theorem enorm_lt_top
added theorem enorm_ne_top
added theorem toNNReal_enorm
added theorem NNReal.nnnorm_eq_self
added theorem Real.enorm_abs
added theorem Real.enorm_eq_ofReal
added theorem Real.enorm_natCast
added theorem Real.enorm_of_nonneg
added theorem Real.le_norm_self
added theorem Real.nnnorm_abs
added theorem Real.nnnorm_natCast
added theorem Real.nnnorm_nnratCast
added theorem Real.nnnorm_ofNat
added theorem Real.nnnorm_of_nonneg
added theorem Real.nnnorm_two
added theorem Real.norm_eq_abs
added theorem Real.norm_natCast
added theorem Real.norm_nnratCast
added theorem Real.norm_ofNat
added theorem Real.norm_of_nonneg
added theorem Real.norm_of_nonpos
added theorem Real.norm_two
added theorem Real.ofReal_le_enorm
added theorem enorm_enorm
added theorem enorm_eq_self
added theorem enorm_norm'
added theorem nnnorm_norm'
added theorem norm_norm'