gluedCoverT'_fst_fst — Mathlib

English

For a glued cover 𝒰, the two-step composition involving fst and snd maps commutes as asserted by the gluing data; i.e., the appropriate pullback maps satisfy the equality given by the gluing relations.

Русский

Для объединенного покрытия 𝒰 соответствующие составления с fst и snd удовлетворяют склейочным соотношениям; т.е. соответствующие отображения пересечения совместимы.

LaTeX

$$$\text{gluedCoverT' 𝒰 x y z} \;\text{ interacts with }\; \mathrm{pullback}(fst) \;\text{ and }\; \mathrm{pullback}(snd) \;\text{ as per the equality in the theorem.}$$$

Lean4

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

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