inf_subgroupOf_right — Mathlib

English

Two subgroups H1, H2 have the same subgroupOf K iff their intersections with K are equal.

Русский

Две подгруппы H1, H2 имеют одинаковый H1.subgroupOf K = H2.subgroupOf K тогда и только если их пересечения с K равны.

LaTeX

$$$ H_1.\\mathrm{subgroupOf} K = H_2.\\mathrm{subgroupOf} K \\iff H_1 \\cap K = H_2 \\cap K $$$

Lean4

@[to_additive (attr := simp)]
theorem inf_subgroupOf_right (H K : Subgroup G) : (H ⊓ K).subgroupOf K = H.subgroupOf K :=
  subgroupOf_inj.2 (inf_right_idem _ _)

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