toSubgroup_le — Mathlib

English

For open subgroups U,V of G, the Subgroup-level inclusion U ≤ V is equivalent to the OpenSubgroup inclusion U ≤ V.

Русский

Для открытых подгрупп U и V группы G включение на уровне подгрупп эквивалентно включению на уровне OpenSubgroup.

LaTeX

$$$$ (U : \\mathrm{Subgroup} G) \\le (V : \\mathrm{Subgroup} G) \\iff U \\le V. $$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem toSubgroup_le : (U : Subgroup G) ≤ (V : Subgroup G) ↔ U ≤ V :=
  Iff.rfl

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