fstPiMap_π — Mathlib

English

For a multicospan index I, the equality I.fstPiMap ≫ Pi.π I.right b = Pi.π I.left _ ≫ I.fst b holds for any b.

Русский

Для индекса мультипопарера выполняется тождество: I.fstPiMap ≫ Pi.π I.right b = Pi.π I.left _ ≫ I.fst b.

LaTeX

$$$I.fstPiMap \;\circ\; \Pi.\pi I.right b = \Pi.\pi I.left (J.fst b) \circ I.fst b$$$

Lean4

@[reassoc (attr := simp)]
theorem fstPiMap_π (b) : I.fstPiMap ≫ Pi.π I.right b = Pi.π I.left _ ≫ I.fst b := by simp [fstPiMap]

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