leftDistributor_ext₂_right — Mathlib

English

A refinement of extensionality where the left distributor extends over a 2-level nested left action; equality is tested componentwise via left distribution and biproduct injections.

Русский

Уточнение экстентности для двойной вложенной левой операции: равенство проверяется по компонентам через левый распределитель и инъекции двупродукта.

LaTeX

$$$$\\forall j, (X \\triangleleft (Y \\triangleleft \\mathrm{biproduct}.\\mathrm{ι}_f j)) \\circ g = (X \\triangleleft (Y \\triangleleft \\mathrm{biproduct}.\\mathrm{ι}_f j)) \\circ h \\Rightarrow g=h,$$$$

Lean4

@[ext]
theorem leftDistributor_ext₂_right {J : Type} [Finite J] {X Y Z : C} {f : J → C} {g h : X ⟶ Y ⊗ (Z ⊗ ⨁ f)}
    (w : ∀ j, g ≫ (Y ◁ (Z ◁ biproduct.π f j)) = h ≫ (Y ◁ (Z ◁ biproduct.π f j))) : g = h :=
  by
  apply (cancel_mono (α_ _ _ _).inv).mp
  ext
  simp [w]

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