lift_π — Mathlib

English

For the morphism j in J, the composition lift f hf with the projection π F j recovers f_j: lift f hf ≫ π F j = f_j.

Русский

Для элемента j ∈ J композиция lift f hf с проекцией π_F j восстанавливает f_j: lift f hf ≫ π_F j = f_j.

LaTeX

$$$\forall j:\, J,\; \text{lift of }f\text{ satisfies }\mathrm{lift}\,f\; hf \;≫\; π F j = f_j$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_π (j : J) : lift f hf ≫ π F j = f j := by apply IsLimit.fac

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