Commit 2024-01-19 09:25 58edd505

View on Github →

chore(CompactOpen): golf (#9829)

  • Add ContinuousMap.compactOpen_eq_mapsTo. I'm going to redefine compactOpen this way in a subsequent PR.
  • Golf/migrate some proofs.

Estimated changes