Commit 2025-02-10 00:54 418896cb

View on Github →

chore(Analysis/Normed/Group): split file (#21554) Split Analysis.Group.Normed.Basic into three files:

  • Analysis.Group.Normed.Basic contains the definitions and the basic results that just use the metric space structure
  • Analysis.Group.Normed.Continuity contains the more advanced results especially the ones that uses the continuity of the norm
  • Analysis.Group.Normed.Subgroup contains the results about subgroups of normed groups. Question. Is there a better name than Analysis.Group.Normed.Continuity?

Estimated changes

deleted theorem Continuous.enorm'
deleted theorem Continuous.nnnorm'
deleted theorem Continuous.norm'
deleted theorem ContinuousAt.enorm'
deleted theorem ContinuousAt.nnnorm'
deleted theorem ContinuousAt.norm'
deleted theorem ContinuousOn.enorm'
deleted theorem ContinuousOn.nnnorm'
deleted theorem ContinuousOn.norm'
deleted theorem ContinuousWithinAt.enorm'
deleted theorem ContinuousWithinAt.norm'
deleted theorem Filter.Tendsto.enorm'
deleted theorem Filter.Tendsto.nnnorm'
deleted theorem Filter.Tendsto.norm'
deleted theorem Inseparable.norm_eq_norm'
deleted theorem Subgroup.coe_norm
deleted theorem Subgroup.norm_coe
deleted theorem SubgroupClass.coe_norm
deleted theorem closure_one_eq
deleted theorem comap_norm_nhdsGT_zero'
deleted theorem comap_norm_nhds_one
deleted theorem continuous_enorm'
deleted theorem continuous_nnnorm'
deleted theorem continuous_norm'
deleted theorem mem_closure_one_iff_norm
deleted theorem squeeze_one_norm'
deleted theorem squeeze_one_norm
deleted theorem tendsto_norm'
deleted theorem tendsto_norm_div_self
deleted theorem tendsto_norm_nhdsNE_one
deleted theorem tendsto_norm_one
added theorem Continuous.enorm'
added theorem Continuous.nnnorm'
added theorem Continuous.norm'
added theorem ContinuousAt.enorm'
added theorem ContinuousAt.nnnorm'
added theorem ContinuousAt.norm'
added theorem ContinuousOn.enorm'
added theorem ContinuousOn.nnnorm'
added theorem ContinuousOn.norm'
added theorem Filter.Tendsto.enorm'
added theorem Filter.Tendsto.nnnorm'
added theorem Filter.Tendsto.norm'
added theorem closure_one_eq
added theorem comap_norm_nhds_one
added theorem continuous_enorm'
added theorem continuous_nnnorm'
added theorem continuous_norm'
added theorem squeeze_one_norm'
added theorem squeeze_one_norm
added theorem tendsto_norm'
added theorem tendsto_norm_div_self
added theorem tendsto_norm_one
added theorem Subgroup.coe_norm
added theorem Subgroup.norm_coe
added theorem SubgroupClass.coe_norm