Commit 2024-09-10 15:21 65a6ba86

View on Github →

chore(AtTopBot): split (#16611)

  • move lemmas depending on ordered monoids to new files;
  • rewrite some proofs about Nat to use Nat-specific lemmas.

Estimated changes

deleted theorem Filter.comap_abs_atTop
deleted theorem Filter.comap_neg_atBot
deleted theorem Filter.comap_neg_atTop
deleted theorem Filter.map_neg_atBot
deleted theorem Filter.map_neg_atTop
deleted theorem Filter.tendsto_atBot_add
deleted theorem Filter.tendsto_atTop_add
deleted theorem Filter.tendsto_pow_atTop
deleted theorem exists_le_mul_self
deleted theorem exists_lt_mul_self
added theorem Filter.comap_abs_atTop
added theorem Filter.comap_neg_atBot
added theorem Filter.comap_neg_atTop
added theorem Filter.map_neg_atBot
added theorem Filter.map_neg_atTop
added theorem exists_le_mul_self
added theorem exists_lt_mul_self