Strictly_Monotone_Mapping_is_Monotone
Disprovedmonotone-mappingsorder-theoryproofwiki
A mapping that is strictly monotone is a monotone mapping.
Preamble
import Mathlib.Order.Monotone.Basic
Formal statement
theorem Strictly_Monotone_Mapping_is_Monotone {α : Type _} {β : Type _} [Preorder α] [Preorder β] {f : α → β} (hf : StrictMono f) : Monotone f := by sorrySource