mathlib3
d6a8e5d7 - feat(topology/compact_open): `simp`-lemmas for `compact_open.gen` (#12267)

Commit

3 years ago

feat(topology/compact_open): `simp`-lemmas for `compact_open.gen` (#12267) This PR adds some basic `simp`-lemmas for `compact_open.gen`.

Author

tb65536

Parents