Commit 2023-03-10 22:18 955518b4

View on Github →

feat: port Analysis.Subadditive (#2772)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Subadditive.lean

added theorem Subadditive.apply_mul_add_le

added theorem Subadditive.eventually_div_lt_of_div_lt

added theorem Subadditive.lim_le_div

added theorem Subadditive.tendsto_lim

added def Subadditive

Modified Mathlib/Order/Filter/AtTopBot.lean

added theorem Filter.Eventually.atTop_of_arithmetic