Zulip Chat Archive

Stream: condensed mathematics

Topic: polyhedral isos


Johan Commelin (Apr 21 2021 at 08:53):

thm95/polyhedral_iso.lean contains a bunch of sorrys that are proof obligations to certain canonical isomorphisms of polyhedral lattices and pseudo normed groups. Feel free to kill some of them.

Johan Commelin (Apr 21 2021 at 08:53):

We'll need most of those for the final bit of homotopy glue, but also for col_exact to show that we are getting some Cech cover.


Last updated: Dec 20 2023 at 11:08 UTC