tensorObj₃'_ext — Mathlib

English

The identifications for the triple tensor object extend via ιTensorObj3' similarly to tensorObj3_eq_ext.

Русский

Идентификации для тройного тензорного объекта распространяются аналогично экстенсивности для ιTensorObj3'.

LaTeX

$$$\text{tensorObj3'_ext }\; (f,g) : f=g\,$$$

Lean4

@[ext (iff := false)]
theorem tensorObj₃'_ext {j : I} {A : C} (f g : tensorObj (tensorObj X₁ X₂) X₃ j ⟶ A)
    [H : HasGoodTensor₁₂Tensor X₁ X₂ X₃]
    (h :
      ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
        ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g) :
    f = g := by
  apply mapBifunctor₁₂BifunctorMapObj_ext (H := H)
  intro i₁ i₂ i₃ hi
  exact h i₁ i₂ i₃ hi

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