coe_lift₂_symm_apply — Mathlib

English

Let F be a function F : Sym2 α → Sym2 β → γ. Then the symmetrized lift satisfies (lift₂.symm F) a1 a2 b1 b2 = F s(a1,a2) s(b1,b2) for all a1,a2 ∈ α and b1,b2 ∈ β.

Русский

Пусть F : Sym2 α → Sym2 β → γ. Тогда (lift₂.symm F) применяется к аргументам a1,a2,b1,b2 так, что для любых a1,a2 ∈ α и b1,b2 ∈ β имеет место равенство (lift₂.symm F) a1 a2 b1 b2 = F (s(a1,a2)) (s(b1,b2)).

LaTeX

$$$ (\\mathrm{lift}_2^{\\mathrm{symm}} F)(a_1,a_2,b_1,b_2) = F\\bigl(s(a_1,a_2),\\ s(b_1,b_2)\\bigr). $$$

Lean4

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

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