English
Realizing a quotient term commutes with the quotient realization map: the realized term in M matches the quotient realization of the term in the quotient structure.
Русский
Реализация терма по факторному множеству совпадает с реализацией терма в факторной структуре.
LaTeX
$$$(t.realize\\ fun i => (\\ Quotient.mk s (x_i))) = \\ Quotient.mk s (t.realize\\ x)$$$
Lean4
theorem realize_quotient_mk' {β : Type*} (t : L.Term β) (x : β → M) :
(t.realize fun i => (⟦x i⟧ : Quotient s)) = ⟦@Term.realize _ _ ps.toStructure _ x t⟧ := by
induction t with
| var => rfl
| func _ _ ih => simp only [ih, funMap_quotient_mk', Term.realize]