English
The RelMap on the quotient mirrors the RelMap on representatives before quotienting.
Русский
RelMap после фактор-множества повторяет RelMap над представителями до факторизации.
LaTeX
$$$\\RelMap R (\\mathrm{quotient\_mk'}(x)) = \\RelMap R x$$$
Lean4
@[simp]
theorem relMap_quotient_mk'_sigma_mk' {n : ℕ} {R : L.Relations n} {i : ι} {x : Fin n → G i} :
RelMap R (fun a => (⟦.mk f i (x a)⟧ : DirectLimit G f)) = RelMap R x :=
by
rw [relMap_quotient_mk']
obtain ⟨k, _, _⟩ := directed_of (· ≤ ·) i (Classical.choose (Finite.bddAbove_range fun _ : Fin n => i))
rw [relMap_equiv_unify G f R (fun a => .mk f i (x a)) i (fun _ ⟨_, hj⟩ => le_of_eq hj.symm)]
rw [unify_sigma_mk_self]