inv_snd_fst — Mathlib

English

The inverse of the diagonal map composed with fst and snd maps yields the canonical fst, illustrating another facet of the compatibility in the diagonal/pullback construction.

Русский

Обратная диагональной карты, составленная с fst и snd, даёт каноническую fst, демонстрируя ещё одну грань совместимости в диагональном/предельном конструировании.

LaTeX

$$$$ (pullbackDiagonalMapIso\ f\ i\ i_1\ i_2)^{−1} \circ fst = fst \circ (i_1 \times i_2) $$$$

Lean4

@[reassoc (attr := simp)]
theorem inv_snd_fst : (pullbackDiagonalMapIso f i i₁ i₂).inv ≫ pullback.snd _ _ ≫ pullback.fst _ _ = pullback.fst _ _ :=
  by
  delta pullbackDiagonalMapIso
  simp

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