exists_unify_eq — Mathlib

English

Equivalence of RelMaps with unify holds by choosing a common index along the directed path.

Русский

Эквивалентность RelMap через unify верна при выборе общего индекса вдоль направленной цепи.

LaTeX

$$$\\RelMap R x = \\RelMap R (unify f x i h)$ for suitable i,h$$

Lean4

theorem exists_unify_eq {α : Type*} [Finite α] {x y : α → Σˣ f} (xy : x ≈ y) :
    ∃ (i : ι) (hx : i ∈ upperBounds (range (Sigma.fst ∘ x))) (hy : i ∈ upperBounds (range (Sigma.fst ∘ y))),
      unify f x i hx = unify f y i hy :=
  by
  obtain ⟨i, hi⟩ := Finite.bddAbove_range (Sum.elim (fun a => (x a).1) fun a => (y a).1)
  rw [Sum.elim_range, upperBounds_union] at hi
  simp_rw [← Function.comp_apply (f := Sigma.fst)] at hi
  exact ⟨i, hi.1, hi.2, funext fun a => (equiv_iff G f _ _).1 (xy a)⟩

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