Theorem Tactic.ComputeAsymptotics.tendsto_nhdsNE_of_tendsto_atTop_nhds_of_eq

Modification history

2026-02-11 11:43
Mathlib/Tactic/ComputeAsymptotics/Lemmas.lean
feat(Tactic/ComputeAsymptotics): lemmas for converting different goals to `Tendsto f atTop l` (#34403) …
Added Tactic.ComputeAsymptotics.tendsto_nhdsNE_of_tendsto_atTop_nhds_of_eqView on Github →