lcurry_apply — Mathlib

English

For all f, m, n with f: M ⊗_R N → P, the currying is compatible with evaluation: (lcurry f) m n = f(m ⊗ n).

Русский

Для всякого f: M ⊗_R N → P и элементов m ∈ M, n ∈ N верно (lcurry f) m n = f(m ⊗ n).

LaTeX

$$$\\forall f:\\ M \\otimes_R N \\to P,\; \\forall m:\\ M,\\; \\forall n:\\ N,\; lcurry\\ R\\ M\\ N\\ P\\ f\\ m\\ n = f(m \\otimes_R n).$$

Lean4

@[simp]
theorem lcurry_apply (f : M ⊗[R] N →ₗ[R] P) (m : M) (n : N) : lcurry R M N P f m n = f (m ⊗ₜ n) :=
  rfl

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