whiskerLeft_left_snd — Mathlib

English

The left whiskering by R along f, when composed with snd, yields snd on the appropriate projections.

Русский

Левое запотягивание по R вдоль f, при композиции с snd даёт snd на нужных проекциях.

LaTeX

$$$ (R \\downarrow f).left \\circ \\mathrm{snd} = \\mathrm{snd} $$$

Lean4

@[reassoc (attr := simp)]
theorem whiskerLeft_left_snd {R S T : Over X} (f : S ⟶ T) :
    (R ◁ f).left ≫ pullback.snd _ _ = pullback.snd _ _ ≫ f.left :=
  limit.lift_π _ _

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