English
The behavior of RelMap under quotients is compatible with lifting to a quotient structure: mapping a RelMap through Quotient.mk equals lifting the map through the structure's RelMap.
Русский
Поведение RelMap при взятии фактор-групп совместимо с переходом к фактор-структуре: отображение RelMap через Quotient.mk эквивалентно отображению через структуру.
LaTeX
$$$(RelMap\\ r\\ fun\\ i => \\ Quotient.mk\\ s\\ (x_i)) \\;\\;\\Leftrightarrow\\;\\; (ps.toStructure s).RelMap\\ r x$$$
Lean4
theorem funMap_quotient_mk' {n : ℕ} (f : L.Functions n) (x : Fin n → M) :
(funMap f fun i => (⟦x i⟧ : Quotient s)) = ⟦@funMap _ _ ps.toStructure _ f x⟧ :=
by
change Quotient.map (@funMap L M ps.toStructure n f) Prestructure.fun_equiv (Quotient.finChoice _) = _
rw [Quotient.finChoice_eq, Quotient.map_mk]
