lift_fac — Mathlib

English

The lift is compatible with composition: lift f g H' after composing with f equals g.

Русский

Лифт совместим с композициями: лифт f g H' после композиции с f равен g.

LaTeX

$$$ lift\; f\; g\; H' \; \Rightarrow \mathrm{comp}(lift\, f\, g) = g $$$

Lean4

@[simp, reassoc]
theorem lift_fac (H' : Set.range g.base ⊆ Set.range f.base) : lift f g H' ≫ f = g := by erw [Category.assoc];
  rw [IsIso.inv_comp_eq]; exact pullback.condition

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