splitFun_inj — Mathlib

English

If two splitFun results are equal, then their f parts and g parts are equal: Eq (splitFun f g) (splitFun f' g') → f = f' ∧ g = g'.

Русский

Если результаты splitFun равны, то их части f и g равны: Eq (splitFun f g) (splitFun f' g') → f = f' ∧ g = g'.

LaTeX

$$$\forall f,g,f',g',\ Eq(\mathrm{splitFun} f g)(\mathrm{splitFun} f' g') \to (f=f' \land g=g')$$$

Lean4

theorem splitFun_inj {α α' : TypeVec (n + 1)} {f f' : drop α ⟹ drop α'} {g g' : last α → last α'}
    (H : splitFun f g = splitFun f' g') : f = f' ∧ g = g' := by
  rw [← dropFun_splitFun f g, H, ← lastFun_splitFun f g, H]; simp

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