mathlib3

ec6d9a73 - feat(topology/algebra/group): definitionally better lattice (#10792)

feat(topology/algebra/group): definitionally better lattice (#10792) This provides `(⊓)`, `⊤`, and `⊥` explicitly such that the associated `to_topological_space` lemmas are definitionally equal.