relMap_quotient_mk'_sigma_mk' — Mathlib

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]

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