ext_fourfold — Mathlib

English

A fourfold extensionality principle for tensor products.

Русский

Четырехфакторная экстрансиональность для тензорного произведения.

LaTeX

$$$\\forall g,h : M \\otimes_R N \\otimes_R P \\otimes_R Q \\to S,\\ (\\forall w\\in M, x\\in N, y\\in P, z\\in Q), g(w\\otimes x\\otimes y\\otimes z)=h(w\\otimes x\\otimes y\\otimes z) \\Rightarrow g=h$.$$

Lean4

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

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