mathlib3
0227820c - feat(topology/algebra/group): added (right/left)_coset_(open/closed) (#11876)

Commit
3 years ago
feat(topology/algebra/group): added (right/left)_coset_(open/closed) (#11876) Added lemmas saying that, in a topological group, cosets of an open (resp. closed) set are open (resp. closed).
Parents
Loading