isComplement_subgroup_left_iff_bijective

English

IsComplement (H) T is equivalent to bijectivity of the map T ↪ G → G/H via quotient.

Русский

IsComplement (H) T эквивалентно биективности отображения T → G/H через фактор-множество.

LaTeX

$$$IsComplement H T \\\\Leftrightarrow Bijective (T.restrict (Quotient.mk'' : G \\\\to Quotient G H))$$$

Lean4

@[to_additive]
theorem isComplement_subgroup_left_iff_bijective :
    IsComplement H T ↔ Bijective (T.restrict (Quotient.mk'' : G → Quotient (QuotientGroup.rightRel H))) :=
  isComplement_subgroup_left_iff_existsUnique_quotientMk''.trans
    (bijective_iff_existsUnique (T.restrict Quotient.mk'')).symm

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