instMin — Mathlib

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'⟩ }⟩

Похожие утверждения