whiskerRight_fst — Mathlib

English

Right whiskering by X preserves the order of fst; i.e., the composition with fst after whiskering equals composing with fst after applying f.

Русский

Правое подсвязывание по X сохраняет порядок fst; композиция с fst после подсвязывания равна композиции с fst после применения f.

LaTeX

$$$$ (f \triangleright X) \circ \mathrm{Prod.fst} = \mathrm{Prod.fst} \circ f. $$$$

Lean4

theorem whiskerRight_fst {A : Cat} {B : Cat} (f : A ⟶ B) (X : Cat) : (f ▷ X) ⋙ Prod.fst _ _ = Prod.fst _ _ ⋙ f :=
  rfl

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