analysis
                                
                                 analysis copied to clipboard
                                
                                    analysis copied to clipboard
                            
                            
                            
                        put together statements about `]x-r,x+r[`
This was a remark made by @zstone1 in the conversation about PR #973 .
"Much of the results we've made will generalize to borel measures, (but without HB it's a bit of a nightmare to try to construct the type of measure + topological space). Factoring out results that we know will be generalizable might be nice to give us a place to start in the future."