coe_lift_symm_apply — Mathlib

English

For any map F from Sym2 α to β, applying lift.symm to F and then evaluating at (a1,a2) yields F evaluated at (a1,a2).

Русский

Для любой карты F: Sym2 α → β, применение lift.symm к F и последующая оценка в (a1,a2) дают F(a1,a2).

LaTeX

$$$\forall F:\mathrm{Sym2}\,\alpha\to\beta\;\forall a_1,a_2:\alpha,\; (\mathrm{lift}.\mathrm{symm}\ F)(a_1,a_2) = F(a_1,a_2)$$$

Lean4

@[simp]
theorem coe_lift_symm_apply (F : Sym2 α → β) (a₁ a₂ : α) : (lift.symm F : α → α → β) a₁ a₂ = F s(a₁, a₂) :=
  rfl

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