lift_comp — Mathlib

English

The triangle formed by the quotient-lift commutes: (hf.lift g h) ∘ f = g.

Русский

Треугольник, образованный склейкой-подъёмом, коммутирует: (hf.lift g h) ∘ f = g.

LaTeX

$$$(hf.lift g h) \\circ f = g$$$

Lean4

/-- The obvious triangle induced by `IsQuotientMap.lift` commutes:
```
     g
  X --→ Z
  |   ↗
f |  / hf.lift g h
  v /
  Y
```
-/
@[simp]
theorem lift_comp : (hf.lift g h).comp f = g := by
  ext
  simpa using h (Function.rightInverse_surjInv _ _)

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