Zulip Chat Archive
Stream: new members
Topic: Area of solution set
Callum Cassidy-Nolan (Mar 06 2022 at 17:53):
Is there a way to ask in lean for the area of a solution set in R^2 ? I have a set of points which satisfy the shaded area (|x + y| < 8 and x, y have the same sign) and I'd like to state in lean that the area of this is equal to something else. Does anyone know if it's possible? image.png
Jakub Kądziołka (Mar 06 2022 at 17:54):
Are you familiar with measure theory?
Callum Cassidy-Nolan (Mar 06 2022 at 17:54):
Not too much, but I'm willing to learn
Callum Cassidy-Nolan (Mar 06 2022 at 17:54):
I know about the metric space
Jakub Kądziołka (Mar 06 2022 at 17:58):
Well, that is the field that actually formally defines what an "area" is. You might be interested in https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/9_area_of_a_circle.lean
Alexandre Rademaker (Mar 20 2025 at 21:05):
Hi @Maja Kądziołka , can you give me more details about this? I am not Mathematics but curious to understand this problem of proof the area define by an inequality is a given number
Alexandre Rademaker (Mar 20 2025 at 21:06):
Link above is broken
Aaron Liu (Mar 20 2025 at 21:27):
Last updated: May 02 2025 at 03:31 UTC