gluedCoverT'_fst_snd — Mathlib

English

For a glued cover 𝒰, the equality involving fst and snd maps holds, expressing commutativity of the relevant pullbacks in the gluing diagram.

Русский

Для склейки 𝒰 равенство между fst и snd отображениями сохраняет равенство в диаграмме склейки.

LaTeX

$$$\text{gluedCoverT' 𝒰 x y z} \;\text{ satisfies the fst-snd compatibility }$$$

Lean4

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

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