comparePkg_eq_extension — Mathlib

English

The underlying map of the comparePkg uniform equivalence agrees with the canonical extension map from continuous coe.

Русский

Базовая карта равномерного эквивалента сравнения совпадает с каноническим продолжением через непрерывное вложение.

LaTeX

$$$(\\mathrm{comparePkg}\\,K)^{\\mathrm{toFun}} = (\\mathrm{extensionAsRingHom}\\,K\\; (\\mathrm{continuous\\_coe}))^{\\mathrm{toFun}}$$$

Lean4

theorem comparePkg_eq_extension (x : UniformSpace.Completion (RatFunc K)) :
    (comparePkg K).toFun x = (extensionAsRingHom K (continuous_coe)).toFun x :=
  rfl

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