mathlib3
201413b9 - chore(topology): Splits topology.basic and topology.continuity (#785)

Commit

6 years ago

chore(topology): Splits topology.basic and topology.continuity (#785) Also, the most basic aspects of continuity are now in topology.basic

References

Author

Patrick Massot

Committer

johoelzl

Parents