lift_eq — Mathlib

English

If two lifts coincide after composition with the canonical map, they are equal.

Русский

Если подъёмы совпадают после композиции с каноническим отображением, они равны.

LaTeX

$$$\forall f\, g\ (hg : g \circ (\mathrm{of}\ I\ M) = f) \Rightarrow g = \mathrm{lift}\ I\ f$$$

Lean4

/-- Uniqueness of lift. -/
theorem lift_eq (f : M →ₗ[R] N) (g : Hausdorffification I M →ₗ[R] N) (hg : g.comp (of I M) = f) : g = lift I f :=
  LinearMap.ext fun x => induction_on x fun x => by rw [lift_of, ← hg, LinearMap.comp_apply]

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