coe_mk — Mathlib

English

For any f and h, the coercion of mk(f,h) equals f; i.e., the underlying function of the circle lift built from f and a proof h is exactly f.

Русский

Для любых f и h, отображение mk(f,h) под действием коэрции равно f; то есть базовая функция круга-функционального подъема, построенного из f и доказательства h, совпадает с f.

LaTeX

$$$\\big( (\\mathrm{mk} f h) \\big)^{\\toFun} = f$; equivalently, $\\mathrm{coe}(\\mathrm{mk}(f,h)) = f$.$$

Lean4

@[simp]
theorem coe_mk (f h) : ⇑(mk f h) = f :=
  rfl

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