appendFun_inj — Mathlib

English

If appending two arrows yields the same appends, then the individual arrows are equal: Eq (appendFun f g) (appendFun f' g') → f = f' ∧ g = g'.

Русский

Если добавление стрелы порождает одинаковые результаты, то составляющие стрелы равны: Eq (appendFun f g) (appendFun f' g') → f = f' ∧ g = g'.

LaTeX

$$Eq (appendFun f g) (appendFun f' g') → (f=f' ∧ g=g')$$

Lean4

theorem appendFun_inj {α α' : TypeVec n} {β β' : Type*} {f f' : α ⟹ α'} {g g' : β → β'} :
    (f ::: g : (α ::: β) ⟹ _) = (f' ::: g' : (α ::: β) ⟹ _) → f = f' ∧ g = g' :=
  splitFun_inj

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