quotientMapSubgroupOfOfLe_mk — Mathlib

English

If A' ≤ B' and A ≤ B, then at the level of elements x in A, the quotient map sends x to the inclusion in B.

Русский

Если A' ≤ B' и A ≤ B, то элемент x ∈ A отображается через факторизованное отображение как включение в B.

LaTeX

$$quotientMapSubgroupOfOfLe h' h x = ↑(Subgroup.inclusion h x : B)$$

Lean4

@[to_additive (attr := simp)]
theorem quotientMapSubgroupOfOfLe_mk {A' A B' B : Subgroup G} [_hAN : (A'.subgroupOf A).Normal]
    [_hBN : (B'.subgroupOf B).Normal] (h' : A' ≤ B') (h : A ≤ B) (x : A) :
    quotientMapSubgroupOfOfLe h' h x = ↑(Subgroup.inclusion h x : B) :=
  rfl

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