Theorems · Theorem · category theory

MvPFunctor.M.bisim

∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (R : P.M α → P.M α → Prop),
  (∀ (x y : P.M α),
      R x y →
        ∃ a f f₁ f₂,
          MvPFunctor.M.dest P x = ⟨a, TypeVec.splitFun f f₁⟩ ∧
            MvPFunctor.M.dest P y = ⟨a, TypeVec.splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)) →
    ∀ (x y : P.M α), R x y → x = y

Defined in

Mathlib.Data.PFunctor.Multivariate.M

Cited by

1 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound