Theorems · Theorem · group theory

QuotientGroup.strictMono_comap_prod_image

∀ {α : Type u_1} [inst : Group α] (s : Subgroup α),
  StrictMono fun t => (Subgroup.comap s.subtype t, QuotientGroup.mk '' ↑t)

Given a subgroup s, the function that sends a subgroup t to the pair consisting of its intersection with s and its image in the quotient α ⧸ s is strictly monotone, even though it is not injective in general.

Defined in

Mathlib.GroupTheory.Coset.Basic

Cited by

1 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Group