Theorem Filter.map_inv_atTop

Modification history

2025-03-18 23:10

Mathlib/Order/Filter/AtTopBot/Group.lean

chore(AtTopBot/Group): use `@[to_additive]` (#22461)

Added Filter.map_inv_atTop View on Github →