Yury G. Kudryashov (Jul 05 2019 at 17:06):
Hi, I'm formalizing rotation numbers, and the proof relies on the following fact: if
f : α → β from an additive monoid to a normed vector space satisfies
∀ x y, ∥f (x + y) - f x - f y∥ < C, then it can be approximated by an additive map.
As far as I understand, the part dealing with limits should go to
What would be a good name for the map
[has_add α] [add_group β] (f : α → β) : α → α → β := λ x y, f (x + y) - f y - f x, and what file would be a good home for this definition/lemmas?
Last updated: May 09 2021 at 10:11 UTC