inv_snd_snd — Mathlib

English

The inverse of the diagonal map composed with snd yields the snd projection, expressing compatibility of the diagonal with the second projection.

Русский

Обратное диагонального отображения, компонуемое со snd, даёт проекцию snd, демонстрируя совместимость диагонали с второй проекцией.

LaTeX

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

Lean4

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

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