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


Last updated: Dec 20 2023 at 11:08 UTC