Commit 2025-01-05 13:11 bbc7c116
View on Github →feat: if f is a measurable group hom, then every point has a neighborhood s such that f '' s is bounded (#20304)
This will be used to solve Cauchy's functional equation.
From LeanCamCombi
feat: if f is a measurable group hom, then every point has a neighborhood s such that f '' s is bounded (#20304)
This will be used to solve Cauchy's functional equation.
From LeanCamCombi