coe_mk — Mathlib

English

If a function f: α → β is monotone, then the bundled order-preserving map built from f via mk has underlying function f.

Русский

Если функция f: α → β монотонна, то упакованный в виде отображения порядка, построенный через mk, имеет как график функцию f.

LaTeX

$$$\\operatorname{coe}(\\operatorname{mk}(f, hf)) = f,$ where $hf$ is a proof that $f$ is monotone.$$

Lean4

@[simp]
theorem coe_mk (f : α → β) (hf : Monotone f) : ⇑(mk f hf) = f :=
  rfl

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