sigma_condition — Mathlib

English

In a multicofork, the fstSigmaMap and sndSigmaMap composed with Sigma.desc K.π yield equal results; i.e., the two coordinate projections are equal after descent.

Русский

В multicofork, отображения fstSigmaMap и sndSigmaMap в сочетании с Sigma.desc K.π дают одинаковый результат; координатные проекции совпадают после спуска.

LaTeX

$$$I.fstSigmaMap \;\circ\; \Sigma.desc K.π = I.sndSigmaMap \;\circ\; \Sigma.desc K.π.$$$

Lean4

@[reassoc (attr := simp)]
theorem sigma_condition : I.fstSigmaMap ≫ Sigma.desc K.π = I.sndSigmaMap ≫ Sigma.desc K.π :=
  by
  ext
  simp

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