unify_sigma_mk_self — Mathlib

English

If you unify with a family coming from Sigma.mk, you recover the original function x, i.e., unify on the encoded sigma returns the original x.

Русский

Если выполнить унификацию для σmk-образа, то вернётся исходная функция x.

LaTeX

$$$\\mathrm{unify}_f(\\lambda a.\\mathrm{mk}_f(i, x(a)), i, h, a) = x(a)$$$

Lean4

@[simp]
theorem unify_sigma_mk_self {α : Type*} {i : ι} {x : α → G i} :
    (unify f (fun a => .mk f i (x a)) i fun _ ⟨_, hj⟩ => _root_.trans (le_of_eq hj.symm) (refl _)) = x :=
  by
  ext a
  rw [unify]
  apply DirectedSystem.map_self

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