doc(topology/open_subgroup): add module docstring (#10111)
doc(topology/open_subgroup): add module docstring (#10111)

Also add a lattice instance.







leanprover-community/mathlib,leanprover-community/mathlib