Theorem Filter.inv_atTop

Modification history

2025-04-04 17:16
Mathlib/Order/Filter/Pointwise.lean
chore: use mixin ordered algebraic typeclasses (part 1) (#20594)
Modified Filter.inv_atTopView on Github →
2023-11-08 13:26
Mathlib/Order/Filter/Pointwise.lean
feat: add lemmas about `Inv.inv` for `Filter`s (#8261)
Added Filter.inv_atTopView on Github →