Commit 2024-01-19 09:25 58edd505
View on Github →chore(CompactOpen): golf (#9829)
- Add
ContinuousMap.compactOpen_eq_mapsTo
. I'm going to redefinecompactOpen
this way in a subsequent PR. - Golf/migrate some proofs.
chore(CompactOpen): golf (#9829)
ContinuousMap.compactOpen_eq_mapsTo
.
I'm going to redefine compactOpen
this way in a subsequent PR.