Commit 2023-11-29 21:38 f3e560f2

View on Github →

refactor: get rid of comap norm atTop (#8262)

Estimated changes

Modified Mathlib/Analysis/Asymptotics/Asymptotics.lean

added theorem Asymptotics.isLittleO_const_id_cobounded

deleted theorem Asymptotics.isLittleO_const_id_comap_norm_atTop

Modified Mathlib/Analysis/Complex/PhragmenLindelof.lean

Modified Mathlib/Analysis/Normed/Field/Basic.lean

added def DilationEquiv.mulLeft

added def DilationEquiv.mulRight

added theorem Filter.comap_mul_left_cobounded

added theorem Filter.comap_mul_right_cobounded

modified theorem Filter.inv_cobounded₀

modified theorem Filter.inv_nhdsWithin_ne_zero

added theorem Filter.map_mul_left_cobounded

added theorem Filter.map_mul_right_cobounded

modified theorem Filter.tendsto_inv₀_cobounded'

modified theorem Filter.tendsto_inv₀_cobounded

modified theorem Filter.tendsto_inv₀_nhdsWithin_ne_zero

modified theorem Filter.tendsto_mul_left_cobounded

modified theorem Filter.tendsto_mul_right_cobounded

added theorem antilipschitzWith_mul_left

added theorem antilipschitzWith_mul_right

Modified Mathlib/Analysis/Normed/Group/Basic.lean

added theorem Filter.inv_cobounded

modified theorem Filter.tendsto_inv_cobounded

added theorem eventually_cobounded_le_norm'

Modified Mathlib/Analysis/SpecialFunctions/Complex/Log.lean

modified theorem Complex.map_exp_comap_re_atTop

Modified Mathlib/Analysis/SpecialFunctions/Exp.lean

added theorem Complex.comap_exp_cobounded

deleted theorem Complex.comap_exp_comap_abs_atTop

modified theorem Complex.tendsto_exp_comap_re_atTop

Modified Mathlib/Topology/MetricSpace/Dilation.lean

added theorem Dilation.comap_cobounded

added theorem Dilation.tendsto_cobounded

Modified Mathlib/Topology/MetricSpace/DilationEquiv.lean

added theorem DilationEquiv.map_cobounded