Commit 2023-11-09 03:06 6032e3a8

View on Github →

feat: inv interchanges cobounded and 𝓝[≠] 0 in normed division rings (#8234)

Estimated changes

Modified Mathlib/Analysis/Normed/Field/Basic.lean

added theorem Filter.inv_cobounded₀

added theorem Filter.inv_nhdsWithin_ne_zero

added theorem Filter.tendsto_inv₀_cobounded'

added theorem Filter.tendsto_inv₀_cobounded

added theorem Filter.tendsto_inv₀_nhdsWithin_ne_zero

Modified Mathlib/Analysis/Normed/Group/Basic.lean

added theorem comap_norm_nhdsWithin_Ioi_zero'

Modified Mathlib/Order/Filter/AtTopBot.lean

added theorem Filter.atTop_basis_Ioi'

Modified Mathlib/Order/Filter/Bases.lean

Modified Mathlib/Topology/Algebra/Order/Field.lean

added theorem inv_atTop₀

added theorem inv_nhdsWithin_Ioi_zero

modified theorem tendsto_inv_atTop_zero'

modified theorem tendsto_inv_zero_atTop

Modified Mathlib/Topology/Order/Basic.lean

added theorem nhdsWithin_Ioi_basis