mapBicone_whisker — Mathlib

English

Applying a functor to a whiskered bicone yields the whiskered mapped bicone.

Русский

Применение функторной операции к bicône с кре́плениями сохраняет структуру через whisker.

LaTeX

$$$F.mapBicone (c.whisker g) = (F.mapBicone c).whisker g$$$

Lean4

theorem mapBicone_whisker {K : Type w₂} {g : K ≃ J} {f : J → C} (c : Bicone f) :
    F.mapBicone (c.whisker g) = (F.mapBicone c).whisker g :=
  rfl

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