mathlib
f7534de0 - feat(topology/nhds_set): add several lemmas (#15957)

Commit

3 years ago

feat(topology/nhds_set): add several lemmas (#15957) Prove `𝓟 s ≤ 𝓝ˢ s` and `𝓝ˢ s = 𝓟 s ↔ is_open s`.

Author

urkud

Parents