Mistake in the "Mathematics in Lean" handbook

Stream: general

[Victor Liu]

Hi there, I am currently following the tutorial on the web version of the "Mathematics in Lean" handbook by Jeremy Avigad, Patrick Massot here. I have noticed a typo in the text:

It is an interesting fact that min distributes over max the way that multiplication distributes over addition, and vice-versa. In other words, on the real numbers, we have the identity min a (max b c) ≤ max (min a b) (min a c) as well as the corresponding version with max and min switched.

The authors meant to write min a (max b c) = max (min a b) (min a c) with a = instead of with a \leq, presumably due to copy-pasting.
image.png

[Victor Liu]

I have found that the source code is available on GitHub, and have created a pull request to fix this typo. https://github.com/avigad/mathematics_in_lean_source/pull/218