pullbackP1Iso_inv_fst — Mathlib

English

The inverse component of P1Iso, when precomposed with the first projection, equals the gluing injection at i.

Русский

Обратный компонент P1Iso, после применения к первой проекции, равно внедрению склейки ι для i.

LaTeX

$$$$ (pullbackP1Iso 𝒰 f g i).inv \; \circ \; \mathrm{fst} = (\text{gluing } 𝒰 f g).ι i $$$$

Lean4

@[simp, reassoc]
theorem pullbackP1Iso_inv_fst (i : 𝒰.I₀) : (pullbackP1Iso 𝒰 f g i).inv ≫ pullback.fst _ _ = (gluing 𝒰 f g).ι i := by
  simp_rw [pullbackP1Iso, pullback.lift_fst]

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