dest'_eq_dest' — Mathlib

English

A variant of dest'_eq_dest' specialized to an equality of x.dest with a specific pair; the result is the same.

Русский

Вариант dest'_eq_dest', уточняющий равенство x.dest с конкретной парой; результат тот же.

LaTeX

$$$\\text{dest'} P h_1 f' = \\text{dest'} P h_2 f'$ при h_1 = h_2$$$

Lean4

theorem dest'_eq_dest' {α : TypeVec n} {x : P.last.M} {a₁ : P.A} {f₁ : P.last.B a₁ → P.last.M}
    (h₁ : PFunctor.M.dest x = ⟨a₁, f₁⟩) {a₂ : P.A} {f₂ : P.last.B a₂ → P.last.M} (h₂ : PFunctor.M.dest x = ⟨a₂, f₂⟩)
    (f' : M.Path P x ⟹ α) : M.dest' P h₁ f' = M.dest' P h₂ f' := by cases h₁.symm.trans h₂; rfl

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