strictMono_comap_prod_map — Mathlib

English

The map H ↦ (H.comap N.subtype, H.map (mk' N)) is strictly monotone with respect to inclusion of subgroups.

Русский

Отображение H ↦ (H.comap N.subtype, H.map (mk' N)) строго моно относительно включения подгрупп.

LaTeX

$$$H_1 \\subsetneq H_2 \\; \\Rightarrow\\; (H_1.comap N.subtype, H_1.map (mk' N)) \\subsetneq (H_2.comap N.subtype, H_2.map (mk' N))$$$

Lean4

@[to_additive QuotientAddGroup.strictMono_comap_prod_map]
theorem strictMono_comap_prod_map : StrictMono fun H : Subgroup G ↦ (H.comap N.subtype, H.map (mk' N)) :=
  strictMono_comap_prod_image N

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