relMap_quotient_mk' — Mathlib

English

The equality of RelMap lifted through quotient mk' coincides with the RelMap in the quotient structure.

Русский

Эквивалентность RelMap после взятия quotient через mk' совпадает с RelMap в фактор-структуре.

LaTeX

$$$(RelMap\\ r)\\ (\\ \\mathrm{fun}\\ i \\mapsto \\ Quotient.mk(s, x_i)) \\;\\equiv\\; (ps.toStructure s).RelMap\\ r x$$$

Lean4

theorem relMap_quotient_mk' {n : ℕ} (r : L.Relations n) (x : Fin n → M) :
    (RelMap r fun i => (⟦x i⟧ : Quotient s)) ↔ @RelMap _ _ ps.toStructure _ r x :=
  by
  change Quotient.lift (@RelMap L M ps.toStructure n r) Prestructure.rel_equiv (Quotient.finChoice _) ↔ _
  rw [Quotient.finChoice_eq, Quotient.lift_mk]

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