whiskerRight_app_apply — Mathlib

English

The whiskering on the right by f acts on the second component in the tensor product.

Русский

WhiskerRight применяет f к второму компоненту тензорного произведения.

LaTeX

$$$ (f \; ▷\; L).app Δ x = ⟨f.app Δ x.1, x.2⟩ $$$

Lean4

@[simp]
theorem whiskerRight_app_apply {K K' : SSet.{u}} (f : K ⟶ K') (L : SSet.{u}) {Δ : SimplexCategoryᵒᵖ}
    (x : (K ⊗ L).obj Δ) : (f ▷ L).app Δ x = ⟨f.app Δ x.1, x.2⟩ :=
  rfl

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