English
The set of open subgroups of G forms a lattice under inclusion, with infimum given by intersection and supremum given by the subgroup generated by the union; the embedding into Subgroup G preserves these lattice operations.
Русский
Множество открытых подпгрупп G образует решётку относительно включения: инфимум — пересечение, супермум — подгруппа, порождённая объединением; вложение в Subgroup G сохраняет эти операции.
LaTeX
$$$U \\wedge V = U \\cap V$, and $U \\vee V$ corresponds to $\\langle U \\cup V \\rangle$ in Subgroup(G).$$
Lean4
@[to_additive]
instance : Lattice (OpenSubgroup G) :=
{ instSemilatticeInfOpenSubgroup,
toSubgroup_injective.semilatticeSup ((↑) : OpenSubgroup G → Subgroup G) fun _ _ ↦ rfl with
toPartialOrder := instPartialOrderOpenSubgroup }
