∀ (α : Type u_2) (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α]
  [inst_2 : ConditionallyCompleteLinearOrderedField β] (x : α),
  LinearOrderedField.inducedMap α β x = sSup (LinearOrderedField.cutMap β x)