lift_comp_of — Mathlib

English

If two linear maps g,h from Hausdorffification I M to N agree after composing with the canonical map of I M, then g = lift I f.

Русский

Если два линейных отображения согласованы после композиции с каноническим отображением I M, то они равны подъёму по f.

LaTeX

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

Lean4

theorem lift_comp_of (f : M →ₗ[R] N) : (lift I f).comp (of I M) = f :=
  LinearMap.ext fun _ => rfl

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