toSubgroup_inf — Mathlib

English

The infimum of open subgroups, when viewed as Subgroups, coincides with the intersection of the underlying Subgroups: (U ⊓ V).toSubgroup = U.toSubgroup ∩ V.toSubgroup.

Русский

Наименьшее между открытыми подгруппами, рассматриваемое как подгруппа, совпадает с пересечением соответствующих подгрупп: (U ⊓ V).toSubgroup = U.toSubgroup ∩ V.toSubgroup.

LaTeX

$$$$(U \\wedge V)^{\\mathrm{toSubgroup}} = U^{\\mathrm{toSubgroup}} \\cap V^{\\mathrm{toSubgroup}}.$$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem toSubgroup_inf : (↑(U ⊓ V) : Subgroup G) = ↑U ⊓ ↑V :=
  rfl

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