English
The meet of two subgroups in the lattice of subgroups is their intersection.
Русский
Наименьшая верхняя грань двух подгрупп в решётке подпгрупп равна их пересечению.
LaTeX
$$$H \wedge K = H \cap K$$$
Lean4
/-- The inf of two subgroups is their intersection. -/
@[to_additive /-- The inf of two `AddSubgroup`s is their intersection. -/
]
instance : Min (Subgroup G) :=
⟨fun H₁ H₂ => { H₁.toSubmonoid ⊓ H₂.toSubmonoid with inv_mem' := fun ⟨hx, hx'⟩ => ⟨H₁.inv_mem hx, H₂.inv_mem hx'⟩ }⟩