asymptotics): generalize `is_*.inv_rev` (#14486)

Commit

3 years ago

feat(analysis/asymptotics/asymptotics): generalize `is_*.inv_rev` (#14486) Use weaker assumption `∀ᶠ x in l, f x = 0 → g x = 0` instead of `∀ᶠ x in l, f x ≠ 0`.

Author

urkud

Parents

8a6a7933

mathlib3 a869df9e - feat(analysis/asymptotics/asymptotics): generalize `is_*.inv_rev` (#14486)

mathlib3
a869df9e - feat(analysis/asymptotics/asymptotics): generalize `is_*.inv_rev` (#14486)