coe_ofStrictMono — Mathlib

English

The underlying function of the embedding produced by ofStrictMono is exactly the original function f.

Русский

Утверждение: базовое отображение, порождаемое в/ofStrictMono, совпадает с исходной функцией f.

LaTeX

$$$\forall x:\alpha:\ (\text{ofStrictMono}(f,h))\,x = f(x)$$

Lean4

@[simp]
theorem coe_ofStrictMono {α β} [LinearOrder α] [Preorder β] {f : α → β} (h : StrictMono f) : ⇑(ofStrictMono f h) = f :=
  rfl

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