tensorObj_ext — Mathlib

English

Extensionality for tensorObj: given f,g: tensorObj X1 X2 j → A, if for all i1,i2 with i1+i2=j the canonical injections ιTensorObj X1 X2 i1 i2 j hi satisfy ιTensorObj X1 X2 i1 i2 j hi ≫ f = ιTensorObj X1 X2 i1 i2 j hi ≫ g, then f = g.

Русский

Экстенсиональность для tensorObj: если для всех пар индексов i1,i2 с i1+i2=j канонические вложения удовлетворяют равенствам, то f=g.

LaTeX

$$$\forall f,g:\; tensorObj X_1 X_2 j \to A,\; (\forall i_1,i_2,\; hi:\, i_1+i_2=j,\; ιTensorObj X_1 X_2 i_1 i_2 j hi \circ f = ιTensorObj X_1 X_2 i_1 i_2 j hi \circ g) \Rightarrow f=g$$$

Lean4

@[ext]
theorem tensorObj_ext {A : C} {j : I} (f g : tensorObj X₁ X₂ j ⟶ A)
    (h : ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j), ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ f = ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ g) : f = g :=
  by
  apply mapObj_ext
  rintro ⟨i₁, i₂⟩ hi
  exact h i₁ i₂ hi

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