dropFun_splitFun — Mathlib

English

Applying splitFun to f and g and then dropping the prefix recovers f: dropFun (splitFun f g) = f.

Русский

Применение splitFun к f и g, затем отброс префикс восстанавливает f: dropFun (splitFun f g) = f.

LaTeX

$$$\mathrm{dropFun}(\mathrm{splitFun} f g) = f$$$

Lean4

@[simp]
theorem dropFun_splitFun {α α' : TypeVec (n + 1)} (f : drop α ⟹ drop α') (g : last α → last α') :
    dropFun (splitFun f g) = f :=
  rfl

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