funMap_unify_equiv — Mathlib

English

The Sigma.mk constructor intertwines with the Embedding map to relate embedded coordinates.

Русский

Конструктор Sigma.mk согласуется с отображением вложений Embedding.

LaTeX

$$$\\mathrm{Sigma.mk}_f(i,x)\\;\\mapsto\\; \\mathrm{Embedding}.map( f_{i,k} )$$$

Lean4

theorem funMap_unify_equiv {n : ℕ} (F : L.Functions n) (x : Fin n → Σˣ f) (i j : ι)
    (hi : i ∈ upperBounds (range (Sigma.fst ∘ x))) (hj : j ∈ upperBounds (range (Sigma.fst ∘ x))) :
    Structure.Sigma.mk f i (funMap F (unify f x i hi)) ≈ .mk f j (funMap F (unify f x j hj)) :=
  by
  obtain ⟨k, ik, jk⟩ := directed_of (· ≤ ·) i j
  refine ⟨k, ik, jk, ?_⟩
  rw [(f i k ik).map_fun, (f j k jk).map_fun, comp_unify, comp_unify]

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