realize_quotient_mk' — Mathlib

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]

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