Commit 2022-05-31 09:48 9e9cc57d

feat(analysis/asymptotics/asymptotics): add is_O_const_iff (#14472)

• use f =ᶠ[l] 0 instead of ∀ᶠ x in l, f x = 0 in is_{O_with,O,o}_zero_right_iff;
• generalize these lemmas from 0 in a normed_group to 0 in a semi_normed_group;
• add is_O.is_bounded_under_le, is_O_const_of_ne, and is_O_const_iff.