prop_tensor — Mathlib

English

If P1 and P2 are object properties and Q is another, and P1 holds at X1 while P2 holds at X2, then Q holds at X1 ⊗ X2 under the tensoring framework TensorLE.

Русский

Если P1 и P2 — свойства объектов, и Q — другое свойство, и P1 верно для X1, P2 для X2, то Q верно для X1 ⊗ X2 в рамках TensorLE.

LaTeX

$$$[TensorLE\\ P_1 P_2 Q] \\; P_1(X_1) \\; P_2(X_2) \\Rightarrow Q(X_1 \\otimes X_2)$$$

Lean4

theorem prop_tensor {P₁ P₂ Q : ObjectProperty C} [TensorLE P₁ P₂ Q] {X₁ X₂ : C} (h₁ : P₁ X₁) (h₂ : P₂ X₂) :
    Q (X₁ ⊗ X₂) :=
  TensorLE.prop_tensor _ _ h₁ h₂

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