liftR_map_last' — Mathlib

English

Bisimulation between Cofix elements: if Dest x and Dest y are related by a lifted relation, then x and y are equal.

Русский

Бисимуляция между элементами Cofix: если Dest x и Dest y связаны поднятым отношением, то x = y.

LaTeX

$$$\\forall x y, r x y \\Rightarrow (\\mathrm{map} (appendFun id (Quot.mk r)) (Cofix.dest x) = \\mathrm{map} (appendFun id (Quot.mk r)) (Cofix.dest y)) \\Rightarrow x = y$$$

Lean4

theorem liftR_map_last' [LawfulMvFunctor F] {α : TypeVec n} {ι} (R : ι → ι → Prop) (x : F (α ::: ι)) (f : ι → ι)
    (hh : ∀ x : ι, R (f x) x) : LiftR' (RelLast' _ R) ((id ::: f) <$$> x) x :=
  by
  have := liftR_map_last R x f id hh
  rwa [appendFun_id_id, MvFunctor.id_map] at this

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