Commit 2023-11-08 13:26 d4e028db

View on Github →

feat: add lemmas about Inv.inv for Filters (#8261)

Estimated changes

Modified Mathlib/Order/Filter/AtTopBot.lean

Modified Mathlib/Order/Filter/Pointwise.lean

added theorem Filter.inv_atTop

Modified Mathlib/Topology/Algebra/GroupWithZero.lean

added theorem nhds_inv₀

added theorem tendsto_inv_iff₀