English
Let H be a subgroup of G. Suppose f: G/H → G assigns to every left coset a representative in G, with f(q) lying in the coset q for all q. Then the canonical representative produced by the left transversal agrees with f on every coset; i.e., the left-quotient representative of q equals f(q) for all q.
Русский
Пусть H– подгруппа группы G. Пусть f: G/H → G задаёт для каждой левой косети её выборочный представитель в G, причём f(q) принадлежит косету q для всех q. Тогда канонический представитель, задаваемый левым трансверсалем, совпадает с f(q) на каждом q.
LaTeX
$$$\\forall q \in G/H,\\; (f(q) : G) \\in q \\quad\\Longrightarrow\\quad (\\text{leftQuotientEquiv}(\\text{isComplement\\_range\\_left}(hf))\\, q : G) = f(q).$$$
Lean4
@[to_additive]
theorem leftQuotientEquiv_apply {f : G ⧸ H → G} (hf : ∀ q, (f q : G ⧸ H) = q) (q : G ⧸ H) :
(leftQuotientEquiv (isComplement_range_left hf) q : G) = f q :=
by
refine (Subtype.ext_iff.mp ?_).trans (Subtype.coe_mk (f q) ⟨q, rfl⟩)
exact (leftQuotientEquiv (isComplement_range_left hf)).apply_eq_iff_eq_symm_apply.mpr (hf q).symm
