English
A left transversal for H in G is a set of representatives picking exactly one element from each left coset gH of H in G.
Русский
Левый трансверсал для подгруппы H в G — это множество представителя, в котором выбрано ровно по одному элементу из каждой левой косеты gH.
LaTeX
$$$\\text{LeftTransversal}(H) := \\{ S \\subseteq G \\;\\big|\\; S \\text{ contains exactly one representative from each left coset of } H \\text{ in } G \\}$$$
Lean4
/-- A left transversal can be viewed as a function mapping each element of the group
to the chosen representative from that left coset. -/
@[to_additive /-- A left transversal can be viewed as a function mapping each element of the group
to the chosen representative from that left coset. -/
]
noncomputable def toLeftFun (hS : IsComplement S H) : G → S :=
leftQuotientEquiv hS ∘ Quotient.mk''
