relMap_unify_equiv — Mathlib

English

RelMaps defined by unite with unify produce the same relation after moving along the directed system.

Русский

RelMap, задаваемые унификацией вместе с unify, сохраняют отношение после переноса по системе.

LaTeX

$$$\\RelMap R (unify f x i h) = \\RelMap R (unify f x j hj)$$$

Lean4

theorem relMap_unify_equiv {n : ℕ} (R : L.Relations n) (x : Fin n → Σˣ f) (i j : ι)
    (hi : i ∈ upperBounds (range (Sigma.fst ∘ x))) (hj : j ∈ upperBounds (range (Sigma.fst ∘ x))) :
    RelMap R (unify f x i hi) = RelMap R (unify f x j hj) :=
  by
  obtain ⟨k, ik, jk⟩ := directed_of (· ≤ ·) i j
  rw [← (f i k ik).map_rel, comp_unify, ← (f j k jk).map_rel, comp_unify]

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