wPathDestLeft_wPathCasesOn — Mathlib

English

A variant of the bisimulation principle stating that if two M-structures are related and their destinations map compatibly under a Quotient-based equivalence, then the two structures are equal.

Русский

Вариант принципа бисимиляции: если две структуры M связаны и их разрушения совместимы относительно эквивалентности через квотирование, то две структуры равны.

LaTeX

$$$\forall {n} (P : MvPFunctor (n+1)) {\alpha} {R} {x} {y}, R x y → (x=y)$ через Quot, подобно предшествующим леммам$$

Lean4

theorem wPathDestLeft_wPathCasesOn {α : TypeVec n} {a : P.A} {f : P.last.B a → P.last.W} (g' : P.drop.B a ⟹ α)
    (g : ∀ j : P.last.B a, P.WPath (f j) ⟹ α) : P.wPathDestLeft (P.wPathCasesOn g' g) = g' :=
  rfl

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