instFunLikeReal — Mathlib

English

There is a canonical function-like structure on CircleDeg1Lift: each element f acts as a real-valued function f.toFun, and the coe to function is faithful, i.e., the underlying function is exactly f.toFun.

Русский

Существуют каноническая структура-функтообразная на CircleDeg1Lift: каждый элемент f действует как вещественно-значная функция f.toFun, и вложение в функцию сохраняет саму функцию.

LaTeX

$$$(\\text{the underlying function of }(\\mathrm{mk} f h)) = f$; more formally, $\\bigl(\\mathrm{toFun}(\\mathrm{CircleDeg1Lift.mk}(f,h))\\bigr) = f$ on the domain.$$

Lean4

instance : FunLike CircleDeg1Lift ℝ ℝ where
  coe f := f.toFun
  coe_injective'
    | ⟨⟨_, _⟩, _⟩, ⟨⟨_, _⟩, _⟩, rfl => rfl

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