Area of solution set

Stream: new members

[Callum Cassidy-Nolan]

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]

Are you familiar with measure theory?

[Callum Cassidy-Nolan]

Not too much, but I'm willing to learn

[Callum Cassidy-Nolan]

I know about the metric space

[Jakub Kądziołka]

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