mathlib
a51c2fd2 - feat(topology/separation): add `eq_on_closure₂` (#16206)

Commit

3 years ago

feat(topology/separation): add `eq_on_closure₂` (#16206) Also use it to golf `submonoid.comm_monoid_topological_closure`.

Author

urkud

Parents