mem_subgroupOf — Mathlib

English

An element h of K belongs to H.subgroupOf K exactly when h viewed as an element of G lies in H.

Русский

Элемент h из K принадлежит H.subgroupOf K тогда и только тогда, когда он, рассматриваемый как элемент G, принадлежит H.

LaTeX

$$$ h \\in H.\\mathrm{subgroupOf} K \\iff (h : G) \\in H $$$

Lean4

@[to_additive]
theorem mem_subgroupOf {H K : Subgroup G} {h : K} : h ∈ H.subgroupOf K ↔ (h : G) ∈ H :=
  Iff.rfl

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