ext_threefold' — Mathlib

English

Another extensionality principle for a different bracketing of a triple tensor product.

Русский

Еще одно правило эктенсиональности для другой скобочной структуры тензорного произведения

LaTeX

$$$\\forall g,h : M \\otimes_R (N \\otimes_R P) \\to Q,\\ (\\forall m\\in M, n\\in N, p\\in P),\\; g(m \\otimes (n \\otimes p)) = h(m \\otimes (n \\otimes p)) \\Rightarrow g=h$.$$

Lean4

theorem ext_threefold' {g h : M ⊗[R] (N ⊗[R] P) →ₗ[R] Q} (H : ∀ x y z, g (x ⊗ₜ (y ⊗ₜ z)) = h (x ⊗ₜ (y ⊗ₜ z))) : g = h :=
  by
  ext x y z
  exact H x y z

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