Maps with bounded coboundaries

Stream: maths

[Yury G. Kudryashov]

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?