## Stream: maths

### Topic: Maps with bounded coboundaries

#### 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 analysis/normed_space.
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