gluedCoverT'_snd_fst — Mathlib

English

In the glued cover setting, the snd_fst compatibility expresses equality of two-step pullbacks involving snd and fst maps.

Русский

В настройке склейки snd_fst выражает равенство отображений пересечения со связами snd и fst.

LaTeX

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

Lean4

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

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