mathematics_in_lean_source
mathematics_in_lean_source copied to clipboard
Topology chapter should teach/warn about products of metric spaces
The metric space on α × β
uses the max
-distance, not the Euclidean distance, and maybe give a forward-reference to the Euclidean distance.