mapTrifunctorMapObj_ext — Mathlib

English

A congruence principle for the inclusions ιMapTrifunctorMapObj with respect to equalities of i₁,i₂,i₃ leading to the same j.

Русский

Принцип согласованности для включений ιMapTrifunctorMapObj относительно равенств индексов, приводящих к одному и тому же j.

LaTeX

$$$ιMapTrifunctorMapObj F p X_1 X_2 X_3 i_1 i_2 i_3 j h = ιMapTrifunctorMapObj F p X_1 X_2 X_3 i_1 i_2 i_3 j h$$$

Lean4

@[ext]
theorem mapTrifunctorMapObj_ext {X₁ : GradedObject I₁ C₁} {X₂ : GradedObject I₂ C₂} {X₃ : GradedObject I₃ C₃} {Y : C₄}
    (j : J) [HasMap ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃) p]
    {φ φ' : mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ Y}
    (h :
      ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p ⟨i₁, i₂, i₃⟩ = j),
        ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ φ = ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ φ') :
    φ = φ' := by
  apply mapObj_ext
  rintro ⟨i₁, i₂, i₃⟩ hi
  apply h

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