English
If f is a symmetric function on pairs from α with values in β, then the lifting to Sym2 agrees with f on canonical pairs.
Русский
Если f — симметричная функция на парах элементов α с значениями в β, то переход к Sym2 согласуется с f на канонических парах.
LaTeX
$$$\\forall \\alpha \\beta\\, (f:\\{ f: \\alpha \\times \\alpha \\to \\beta \\;\\vert\\; \\forall a_1,a_2, f(a_1,a_2)=f(a_2,a_1)\\})\\;\\forall a_1,a_2:\\alpha,\\; \\mathrm{lift}\\,f\\,s(a_1,a_2) = f(a_1,a_2)$$$
Lean4
@[simp]
theorem lift_mk (f : { f : α → α → β // ∀ a₁ a₂, f a₁ a₂ = f a₂ a₁ }) (a₁ a₂ : α) :
lift f s(a₁, a₂) = (f : α → α → β) a₁ a₂ :=
rfl
