pullbackFstιToV_fst — Mathlib

English

Variant expression of the fst-to-V interaction with fst in the pullback construction.

Русский

Вариант выражения взаимодействия fst-to-V с fst в конструкции обратного.

LaTeX

$$$ pullbackFstιToV 𝒰 f g i j \\;\\gg\\; \\mathrm{fst} \\_ \\_ = \\mathrm{snd} \\_ \\_$$

Lean4

@[simp, reassoc]
theorem pullbackFstιToV_fst (i j : 𝒰.I₀) : pullbackFstιToV 𝒰 f g i j ≫ pullback.fst _ _ = pullback.snd _ _ := by
  simp [pullbackFstιToV, p1]

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