comp_unify — Mathlib

English

Composing the embedding f i→j with unify along x is the same as unifying at level j for the transformed x.

Русский

Сочетание вложения и унификации соответствует унификации на уровне j для преобразованного x.

LaTeX

$$$f_{i,j}\\circ\\mathrm{unify}_f(x,i,h)=\\mathrm{unify}_f(x,j,\\lambda k,\\; k\\ge j\\,\\Rightarrow\\dots)\\circ$$$

Lean4

theorem comp_unify {α : Type*} {x : α → Σˣ f} {i j : ι} (ij : i ≤ j) (h : i ∈ upperBounds (range (Sigma.fst ∘ x))) :
    f i j ij ∘ unify f x i h = unify f x j fun k hk => _root_.trans (mem_upperBounds.1 h k hk) ij :=
  by
  ext a
  simp [unify, DirectedSystem.map_map]

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