ext_fourfold' — Mathlib

English

Another structural extensionality principle for a differently nested tensor product.

Русский

Другой принцип экстрансиональности для иначе вложенного тензорного произведения.

LaTeX

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

Lean4

/-- Two linear maps (M ⊗ N) ⊗ (P ⊗ Q) → S which agree on all elements of the
form (m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q) are equal. -/
theorem ext_fourfold' {φ ψ : M ⊗[R] N ⊗[R] (P ⊗[R] Q) →ₗ[R] S}
    (H : ∀ w x y z, φ (w ⊗ₜ x ⊗ₜ (y ⊗ₜ z)) = ψ (w ⊗ₜ x ⊗ₜ (y ⊗ₜ z))) : φ = ψ :=
  by
  ext m n p q
  exact H m n p q

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