English
The transfer transversal is a left transversal of H in G formed by taking the range of transferSet and equipping it with the left-quotient complement property.
Русский
Передачи трансверсаль образуются как левая трансверсаль подгруппы H в G, состоящая из элементов transferSet и обладающая свойством дополнения в левой норме.
LaTeX
$$$\mathrm{transferTransversal}(H,g) = \langle\mathrm{transferSet}(H,g),\; \mathrm{isComplement\_range\_left}(\mathrm{coe\_transferFunction}(g))\rangle$$$
Lean4
/-- The transfer transversal as a set. Contains elements of the form `g ^ k • g₀` for fixed choices
of representatives `g₀` of fixed choices of representatives `q₀` of `⟨g⟩`-orbits in `G ⧸ H`. -/
def transferSet : Set G :=
Set.range (transferFunction H g)
