gluedCoverT'_snd_snd — Mathlib

English

For a glued cover 𝒰, the snd_snd identity asserts a commutativity relation among pullbacks via snd maps in the gluing diagram.

Русский

Для склейки 𝒰 идентность snd_snd задаёт тождественную диаграмму совместимости между вытягиваниями через snd.

LaTeX

$$$\text{gluedCoverT' 𝒰 x y z} \;\rightarrow\; \text{pullback.snd}(fst) \circ \text{pullback.snd}(fst) = \text{pullback.fst}(fst) \circ \text{pullback.fst}(fst)$$$

Lean4

@[simp, reassoc]
theorem gluedCoverT'_snd_snd (x y z : 𝒰.I₀) :
    gluedCoverT' 𝒰 x y z ≫ pullback.snd _ _ ≫ pullback.snd _ _ = pullback.fst _ _ ≫ pullback.fst _ _ := by
  delta gluedCoverT'; simp

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