Commit 2024-09-07 09:03 19b4c40b

View on Github →

feat(AtTopBot): generalize more to Preorder (#16548)

  • Generalize Filter.map_atTop_eq_of_gc and corollaries to a Preorder.
  • Add Nat.map_cast_int_atTop.

Estimated changes

modified theorem Filter.atBot_Iic_eq
modified theorem Filter.atBot_Iio_eq
modified theorem Filter.atTop_Ici_eq
modified theorem Filter.atTop_Ioi_eq
modified theorem Filter.map_atBot_eq_of_gc
modified theorem Filter.map_atTop_eq_of_gc
modified theorem Filter.map_val_Ici_atTop
modified theorem Filter.map_val_Iic_atBot
modified theorem Filter.map_val_Iio_atBot
modified theorem Filter.map_val_Ioi_atTop
modified theorem Filter.tendsto_Ici_atTop
modified theorem Filter.tendsto_Iic_atBot
modified theorem Filter.tendsto_Iio_atBot
modified theorem Filter.tendsto_Ioi_atTop
added theorem Nat.map_cast_int_atTop