pullback_refine — Mathlib

English

The forward application of the equivalence to the element yields the component on I.

Русский

Прямое применение эквивалентности к элементу даёт компонент на I.

LaTeX

$$$\text{equiv apply}: x \mapsto \text{component on } I$$$

Lean4

@[simp]
theorem pullback_refine {Y X : C} {P : Cᵒᵖ ⥤ D} {S T : J.Cover X} (h : S ⟶ T) (f : Y ⟶ X) (x : Meq P T) :
    (x.pullback f).refine ((J.pullback f).map h) = (refine x h).pullback _ :=
  rfl

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