Commit 2022-10-01 23:57 852b23b5

chore(topology,analysis): make the sup metric and norm computable (#16570) To make this work, we replace max with sup in the implementation (the two are defeq, but the former has stronger typeclass arguments), and add some missing shortcut instances for ennreal which are needed for the emetric structure. As a result, we can can now perform useless "computation"s like:

#eval ∥((3 : ℤ), (4 : ℤ))∥
-- real.of_cauchy (sorry /- 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, ... -/)

(this isn't totally useless; it's enough to inform the reader that they're not looking at a euclidean norm, which is a common source of confusion)