Theorem Filter.tendsto_inv₀_nhdsWithin_ne_zero

Modification history

2024-09-05 04:39

Mathlib/Analysis/Normed/Field/Basic.lean

chore: split Analysis.Normed.Field.Basic (#16479)

Modified Filter.tendsto_inv₀_nhdsWithin_ne_zero View on Github →

2023-11-29 21:38

Mathlib/Analysis/Normed/Field/Basic.lean

refactor: get rid of `comap norm atTop` (#8262)

Modified Filter.tendsto_inv₀_nhdsWithin_ne_zero View on Github →

2023-11-09 03:06

Mathlib/Analysis/Normed/Field/Basic.lean

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

Added Filter.tendsto_inv₀_nhdsWithin_ne_zero View on Github →