transferTransversal_apply — Mathlib

English

A version of the previous relation transported along orbits yields a similar equality with orbitRel quotients.

Русский

Версия предыдущего соотношения, переносимая вдоль орбит, даёт аналогичное тождество для фактор-группы орбит.

LaTeX

$$$\uparrow\bigl((\mathrm{transferTransversal}(H,g)).2.leftQuotientEquiv (g^{(cast k)} \cdot q.out)\bigr) = g^{(cast k)} \cdot q.out$$$

Lean4

theorem transferTransversal_apply (q : G ⧸ H) :
    ↑((transferTransversal H g).2.leftQuotientEquiv q) = transferFunction H g q :=
  IsComplement.leftQuotientEquiv_apply (coe_transferFunction g) q

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