isComplement_subgroup_left_iff_existsUnique_quotientMk''

English

IsComplement H T is equivalent to: for every q in G/H, there exists a unique t ∈ T with Quot.mk'' t.1 = q.

Русский

IsComplement H T эквивалентно: для каждого q в G/H существует уникальный t ∈ T такой, что Quot.mk'' t.1 = q.

LaTeX

$$$IsComplement H T \\\\Leftrightarrow \\\\forall q : Quotient (QuotientGroup.rightRel H), \\\\exists! t : T, Quotient.mk'' t.1 = q$$$

Lean4

@[to_additive]
theorem isComplement_subgroup_left_iff_existsUnique_quotientMk'' :
    IsComplement H T ↔ ∀ q : Quotient (QuotientGroup.rightRel H), ∃! t : T, Quotient.mk'' t.1 = q := by
  simp_rw [isComplement_iff_existsUnique_mul_inv_mem, SetLike.mem_coe, ← QuotientGroup.rightRel_apply, ← Quotient.eq'',
    Quotient.forall]

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