hom_ext — Mathlib

English

If f is the map of a morphism in the fiber p.obj a → p.obj b and φ: a ⟶ b is a lifting such that p.IsHomLift f φ holds, then f equals p.map φ.

Русский

Если f — отображение стрелки в фибре p и φ: a ⟶ b является поднятием, удовлетворяющим p.IsHomLift f φ, тогда f = p.map φ.

LaTeX

$$$f = p.map \\; \\varphi$ (under the assumption $[p.IsHomLift f \\varphi]$).$$

Lean4

@[ext]
theorem hom_ext {a b : Fiber p S} {φ ψ : a ⟶ b} (h : fiberInclusion.map φ = fiberInclusion.map ψ) : φ = ψ :=
  Subtype.ext h

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