Commit 2024-06-18 08:57 0fc7ecaa

View on Github →

chore(Analysis/Normed/Group): Move boundedness lemmas (#13895) Split a new file Analysis.Normed.Group.Bounded off Analysis.Normed.Group.Basic. Basically no imports get shaved off in this PR, but it's preparing the way to #13713.

Estimated changes

Modified Mathlib.lean

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

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

deleted theorem Bornology.IsBounded.exists_pos_norm_le'

deleted theorem Bornology.IsBounded.exists_pos_norm_lt'

deleted theorem Continuous.bounded_above_of_compact_support

deleted theorem Filter.HasBasis.cobounded_of_norm'

deleted theorem Filter.Tendsto.op_one_isBoundedUnder_le'

deleted theorem Filter.Tendsto.op_one_isBoundedUnder_le

deleted theorem Filter.hasBasis_cobounded_norm'

deleted theorem Filter.inv_cobounded

deleted theorem Filter.tendsto_inv_cobounded

deleted theorem HasCompactMulSupport.exists_bound_of_continuous

deleted theorem HasCompactMulSupport.exists_pos_le_norm

deleted theorem IsCompact.exists_bound_of_continuousOn'

deleted theorem NormedCommGroup.cauchySeq_iff

deleted theorem comap_norm_atTop'

deleted theorem eventually_cobounded_le_norm'

deleted theorem isBounded_iff_forall_norm_le'

deleted theorem tendsto_norm_atTop_iff_cobounded'

deleted theorem tendsto_norm_cobounded_atTop'

deleted theorem tendsto_norm_cocompact_atTop'

Created Mathlib/Analysis/Normed/Group/Bounded.lean

added theorem Bornology.IsBounded.exists_pos_norm_le'

added theorem Bornology.IsBounded.exists_pos_norm_lt'

added theorem Continuous.bounded_above_of_compact_support

added theorem Filter.HasBasis.cobounded_of_norm'

added theorem Filter.Tendsto.op_one_isBoundedUnder_le'

added theorem Filter.Tendsto.op_one_isBoundedUnder_le

added theorem Filter.hasBasis_cobounded_norm'

added theorem Filter.inv_cobounded

added theorem Filter.tendsto_inv_cobounded

added theorem HasCompactMulSupport.exists_bound_of_continuous

added theorem HasCompactMulSupport.exists_pos_le_norm

added theorem IsCompact.exists_bound_of_continuousOn'

added theorem NormedCommGroup.cauchySeq_iff

added theorem comap_norm_atTop'

added theorem eventually_cobounded_le_norm'

added theorem isBounded_iff_forall_norm_le'

added theorem tendsto_norm_atTop_iff_cobounded'

added theorem tendsto_norm_cobounded_atTop'

added theorem tendsto_norm_cocompact_atTop'

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