Order_Embedding_into_Image_is_Isomorphism
Provedorder-embeddingsorder-isomorphismsproofwiki
An order embedding from S to T induces an order isomorphism from S to its image in T.
Preamble
import Mathlib.Order.Hom.Basic import Mathlib.Data.Set.Function
Formal statement
theorem Order_Embedding_into_Image_is_Isomorphism {α : Type _} {β : Type _} [Preorder α] [Preorder β] (φ : α ↪o β) : Nonempty (α ≃o Set.range φ) := by sorrySource