Theorem Asymptotics.isLittleO_irrefl

Modification history

2026-08-24 06:52

Mathlib/Analysis/Asymptotics/Basic.lean

refactor(Analysis/Asymptotics): split long file Defs.lean (#42997) …

Modified Asymptotics.isLittleO_irrefl View on Github →

2023-04-12 19:26

Mathlib/Analysis/Asymptotics/Asymptotics.lean

feat: port Analysis.Asymptotics.Asymptotics (#3393) …

Added Asymptotics.isLittleO_irrefl View on Github →